Theorems · Theorem · measure theory

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 η],
  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 η) →
            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.

Defined in

Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsFiniteMeasureMeasureTheory.IsFiniteMeasureProbabilityTheory.IsMarkovKernelProbabilityTheory.IsMarkovKernel