Theorems · Theorem · information theory

ConvexOn.map_condExp_rnDeriv_le

∀ {𝓧 : Type u_1} {m m𝓧 : MeasurableSpace 𝓧} {μ ν : MeasureTheory.Measure 𝓧} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν] {f : ℝ → ℝ} (hm : m ≤ m𝓧),
  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 (ν[fun x => (μ.rnDeriv ν x).toReal | m] x)) ≤ᵐ[ν.trim hm] ν[fun x => f (μ.rnDeriv ν x).toReal | m]

Defined in

Mathlib.InformationTheory.KullbackLeibler.DataProcessing

Cited by

3 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsFiniteMeasureMeasureTheory.IsFiniteMeasure