Theorems · Theorem · information theory

ConvexOn.integrable_comp_rnDeriv_trim

∀ {𝓧 : 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) ν →
            MeasureTheory.Integrable (fun x => f ((μ.trim hm).rnDeriv (ν.trim hm) x).toReal) (ν.trim hm)

Defined in

Mathlib.InformationTheory.KullbackLeibler.DataProcessing

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsFiniteMeasureMeasureTheory.IsFiniteMeasure