Theorems · Theorem · information theory

ConvexOn.comp_rnDeriv_map_le

∀ {𝓧 : Type u_1} {𝓨 : Type u_2} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {μ ν : MeasureTheory.Measure 𝓧}
  [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] {f : ℝ → ℝ} {g : 𝓧 → 𝓨},
  μ.AbsolutelyContinuous ν →
    Measurable g →
      MeasureTheory.StronglyMeasurable f →
        ConvexOn ℝ (Set.Ici 0) f →
          ContinuousWithinAt f (Set.Ici 0) 0 →
            MeasureTheory.Integrable (fun x => f (μ.rnDeriv ν x).toReal) ν →
              (fun x => f ((MeasureTheory.Measure.map g μ).rnDeriv (MeasureTheory.Measure.map g ν) (g x)).toReal) ≤ᵐ[ν]
                ν[fun x => f (μ.rnDeriv ν x).toReal | MeasurableSpace.comap g m𝓨]

Defined in

Mathlib.InformationTheory.KullbackLeibler.DataProcessing

Cited by

1 results in Mathlib

Foundations

Depth 308 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasureTheory.IsFiniteMeasureMeasureTheory.IsFiniteMeasure