Averaging conditional probability bounds #
This file records the elementary final step used after the latent two-point decomposition: an almost-everywhere event bound for the conditional Markov kernel survives averaging over a probability law.
theorem
Feige.measureReal_bind_apply_le
{A : Type u_1}
{B : Type u_2}
[MeasurableSpace A]
[MeasurableSpace B]
(κ : ProbabilityTheory.Kernel A B)
[ProbabilityTheory.IsMarkovKernel κ]
(ν : MeasureTheory.Measure A)
[MeasureTheory.IsProbabilityMeasure ν]
{s : Set B}
(hs : MeasurableSet s)
{c : ℝ}
(hc0 : 0 ≤ c)
(hc : ∀ᵐ (a : A) ∂ν, (κ a).real s ≤ c)
:
An almost-everywhere real-valued probability bound for the fibres of a Markov kernel is inherited by the mixture measure.