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 ∂ν.
• ConvexOn.integrable_apply_rnDeriv_of_integrable_compProd: for f a convex function on [0, ∞), if f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b)) is integrable, then f (μ.rnDeriv ν a) is integrable.

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 ∂ν.

theorem MeasureTheory.lintegral_rnDeriv_compProd {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {μ : Measure 𝓧} {𝓨 : Type u_2} {m𝓨 : MeasurableSpace 𝓨} {κ η : ProbabilityTheory.Kernel 𝓧 𝓨} [IsFiniteMeasure μ] [ProbabilityTheory.IsSFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η] (hκη : (μ.compProd κ).AbsolutelyContinuous (μ.compProd η)) : ∀ᵐ (a : 𝓧) ∂μ, ∫⁻ (b : 𝓨), (μ.compProd κ).rnDeriv (μ.compProd η) (a, b) ∂η a = (κ a) Set.univ

theorem ConvexOn.apply_rnDeriv_ae_le_integral {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {μ ν : MeasureTheory.Measure 𝓧} {𝓨 : Type u_2} {m𝓨 : MeasurableSpace 𝓨} {κ η : ProbabilityTheory.Kernel 𝓧 𝓨} {f : ℝ → ℝ} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] [ProbabilityTheory.IsMarkovKernel κ] [ProbabilityTheory.IsMarkovKernel η] (hf : MeasureTheory.StronglyMeasurable f) (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (hf_cont_at : ContinuousWithinAt f (Set.Ici 0) 0) (h_int : MeasureTheory.Integrable (fun (p : 𝓧 × 𝓨) => f ((μ.compProd κ).rnDeriv (ν.compProd η) p).toReal) (ν.compProd η)) (hκη : (μ.compProd κ).AbsolutelyContinuous (μ.compProd η)) : (fun (a : 𝓧) => f (μ.rnDeriv ν a).toReal) ≤ᵐ[ν] fun (a : 𝓧) => ∫ (b : 𝓨), f ((μ.compProd κ).rnDeriv (ν.compProd η) (a, b)).toReal ∂η a

The value of a convex function applied at a Radon-Nikodym derivative can be bounded by the integral of the function applied to the Radon-Nikodym derivative of composition-products.

theorem ConvexOn.integrable_apply_rnDeriv_of_integrable_compProd {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {μ ν : MeasureTheory.Measure 𝓧} {𝓨 : Type u_2} {m𝓨 : MeasurableSpace 𝓨} {κ η : ProbabilityTheory.Kernel 𝓧 𝓨} {f : ℝ → ℝ} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] [ProbabilityTheory.IsMarkovKernel κ] [ProbabilityTheory.IsMarkovKernel η] (hf : MeasureTheory.StronglyMeasurable f) (hf_cvx : ConvexOn ℝ (Set.Ici 0) f) (hf_cont_at : ContinuousWithinAt f (Set.Ici 0) 0) (hf_int : MeasureTheory.Integrable (fun (p : 𝓧 × 𝓨) => f ((μ.compProd κ).rnDeriv (ν.compProd η) p).toReal) (ν.compProd η)) (hκη : (μ.compProd κ).AbsolutelyContinuous (μ.compProd η)) : MeasureTheory.Integrable (fun (a : 𝓧) => f (μ.rnDeriv ν a).toReal) ν

For f a convex function on Ici 0, if f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b)) is integrable, then f (μ.rnDeriv ν a) is integrable.