Integrals of functions of Radon-Nikodym derivatives

Main statements

• mul_le_integral_rnDeriv_of_ac: for a convex continuous function f on [0, ∞), if μ is absolutely continuous with respect to ν, then ν.real univ * f (μ.real univ / ν.real univ) ≤ ∫ x, f (μ.rnDeriv ν x).toReal ∂ν.

theorem MeasureTheory.Measure.integrable_toReal_rnDeriv {α : Type u_1} {mα : MeasurableSpace α} {μ ν : Measure α} [IsFiniteMeasure μ] : Integrable (fun (x : α) => (μ.rnDeriv ν x).toReal) ν

theorem MeasureTheory.le_integral_rnDeriv_of_ac {α : Type u_1} {mα : MeasurableSpace α} {μ ν : Measure α} {f : ℝ → ℝ} [IsFiniteMeasure μ] [IsProbabilityMeasure ν] (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (hf_cont : ContinuousWithinAt f (Set.Ici 0) 0) (hf_int : Integrable (fun (x : α) => f (μ.rnDeriv ν x).toReal) ν) (hμν : μ.AbsolutelyContinuous ν) : f (μ.real Set.univ) ≤ ∫ (x : α), f (μ.rnDeriv ν x).toReal ∂ν

For a convex continuous function f on [0, ∞), if μ is absolutely continuous with respect to a probability measure ν, then f μ.real univ ≤ ∫ x, f (μ.rnDeriv ν x).toReal ∂ν.

theorem MeasureTheory.mul_le_integral_rnDeriv_of_ac {α : Type u_1} {mα : MeasurableSpace α} {μ ν : Measure α} {f : ℝ → ℝ} [IsFiniteMeasure μ] [IsFiniteMeasure ν] (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (hf_cont : ContinuousWithinAt f (Set.Ici 0) 0) (hf_int : Integrable (fun (x : α) => f (μ.rnDeriv ν x).toReal) ν) (hμν : μ.AbsolutelyContinuous ν) : ν.real Set.univ * f (μ.real Set.univ / ν.real Set.univ) ≤ ∫ (x : α), f (μ.rnDeriv ν x).toReal ∂ν

For a convex continuous function f on [0, ∞), if μ is absolutely continuous with respect to ν, then ν.real univ * f (μ.real univ / ν.real univ) ≤ ∫ x, f (μ.rnDeriv ν x).toReal ∂ν.