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 (ν univ).toReal * f ((μ univ).toReal / (ν univ).toReal) ≤ ∫ x, f (μ.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 (μ Set.univ).toReal ≤ ∫ (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 (μ univ).toReal ≤ ∫ 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 ν) : (ν Set.univ).toReal * f ((μ Set.univ).toReal / (ν Set.univ).toReal) ≤ ∫ (x : α), f (μ.rnDeriv ν x).toReal ∂ν

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