Theorems · Theorem · information theory

ConvexOn.comp_rnDeriv_trim_le

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