Theorems · Theorem · measure theory

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 η],
  MeasureTheory.StronglyMeasurable f →
    ConvexOn ℝ (Set.Ici 0) f →
      ContinuousWithinAt f (Set.Ici 0) 0 →
        MeasureTheory.Integrable (fun p => f ((μ.compProd κ).rnDeriv (ν.compProd η) p).toReal) (ν.compProd η) →
          (μ.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.

Defined in

Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsFiniteMeasureMeasureTheory.IsFiniteMeasureProbabilityTheory.IsMarkovKernelProbabilityTheory.IsMarkovKernel