Averaging a conditional event-error bound

1. Fix a measurable event t. Kernel measurability makes \(k_t(x)=K(x,t)\) and \(l_t(x)=L(x,t)\) measurable real functions. Markov normalization gives \(0\le k_t,l_t\le1\); since \(μ\) is a probability measure, both are integrable.

2. The bind/composition law gives \[\begin{gathered}(K\circ_m\mu)(t)=\int k_t\,d\mu,\\(L\circ_m\mu)(t)=\int l_t\,d\mu.\end{gathered}\] In Lean the underlying masses are extended nonnegative reals. Their finiteness, supplied by the probability-kernel assumptions, justifies conversion to real integrals; the totalized toReal API is not used as if infinity were finite.

3. The two integrable event functions can be subtracted inside the integral. The integral triangle inequality gives \[\left|\int k_t\,d\mu-\int l_t\,d\mu\right|\le\int|k_t-l_t|\,d\mu.\] The absolute difference is integrable as well.

4. The common almost-everywhere hypothesis supplies \(|k_t-l_t|\le\varepsilon\) almost everywhere for this event. Monotonicity for integrable real functions yields \[|(K\circ_m\mu)(t)-(L\circ_m\mu)(t)|\le\int\varepsilon\,d\mu.\] No measurable supremum over all events is needed, and no new global nonnegativity premise on \(ε\) is inserted.

/- SamplingOptimisationGeometryBench public-dev reference.
   Reuses the existing project proof; retain LICENSE and NOTICE. -/
import AutoSamplingTheory.TechnicalLemmas.Probability.KernelTotalVariation

open MeasureTheory ProbabilityTheory Set Finset
open scoped ProbabilityTheory BigOperators

example
    {A B : Type*} [MeasurableSpace A] [MeasurableSpace B]
    (μ : Measure A) [IsProbabilityMeasure μ]
    (K L : Kernel A B) [IsMarkovKernel K] [IsMarkovKernel L]
    (ε : A → ℝ) (hε : Integrable ε μ)
    (hbound : ∀ᵐ x ∂μ, ∀ s, MeasurableSet s →
      |(K x).real s - (L x).real s| ≤ ε x) :
    ∀ t, MeasurableSet t →
      |(K ∘ₘ μ).real t - (L ∘ₘ μ).real t| ≤ ∫ x, ε x ∂μ := by
  intro t ht
  have hint (M : Kernel A B) [IsMarkovKernel M] :
      Integrable (fun x => (M x).real t) μ := by
    apply (integrable_const (1 : ℝ)).mono'
      (M.measurable_coe ht).ennreal_toReal.aestronglyMeasurable
    exact Filter.Eventually.of_forall fun x => by
      rw [Real.norm_eq_abs, abs_of_nonneg ENNReal.toReal_nonneg]
      exact (measureReal_le_one : (M x).real t ≤ 1)
  have happly (M : Kernel A B) [IsMarkovKernel M] :
      (M ∘ₘ μ).real t = ∫ x, (M x).real t ∂μ := by
    change (Measure.bind μ M t).toReal = ∫ x, (M x t).toReal ∂μ
    rw [Measure.bind_apply ht M.aemeasurable]
    exact (integral_toReal (M.measurable_coe ht).aemeasurable
      (Filter.Eventually.of_forall fun x => measure_lt_top (M x) t)).symm
  rw [happly K, happly L, ← integral_sub (hint K) (hint L)]
  exact abs_integral_le_integral_abs.trans <|
    integral_mono_ae ((hint K).sub (hint L)).abs hε <|
      hbound.mono fun x hx => hx t ht

1. Establishes event measurability and boundedness by one, hence integrability under the probability input law. (1 point)
2. Uses the bind law with finite event masses to justify the real expectation identities. (1 point)
3. Justifies integral subtraction and the triangle inequality using integrability, not a formal subtraction of infinities. (1 point)
4. Applies the common almost-everywhere event bound and integrability of \(ε\) without assuming a measurable TV supremum or an expected-cost theorem. (1 point)

/- SamplingOptimisationGeometryBench public-dev reference.
   Reuses the existing project proof; retain LICENSE and NOTICE. -/
import AutoSamplingTheory.TechnicalLemmas.Probability.KernelTotalVariation

open MeasureTheory ProbabilityTheory Set Finset
open scoped ProbabilityTheory BigOperators

example
    {A B : Type*} [MeasurableSpace A] [MeasurableSpace B]
    (μ : Measure A) [IsProbabilityMeasure μ]
    (K L : Kernel A B) [IsMarkovKernel K] [IsMarkovKernel L]
    (ε : A → ℝ) (hε : Integrable ε μ)
    (hbound : ∀ᵐ x ∂μ, ∀ s, MeasurableSet s →
      |(K x).real s - (L x).real s| ≤ ε x) :
    ∀ t, MeasurableSet t →
      |(K ∘ₘ μ).real t - (L ∘ₘ μ).real t| ≤ ∫ x, ε x ∂μ := by
  -- Replace this comment with your proof.

Download task template

The reference builds integrability separately for each fixed event from kernel measurability, Markov mass bounds and the probability input law. The bind_apply and integral_toReal steps expose the finite-mass conversion. It then uses integral_sub, abs_integral_le_integral_abs and integral_mono_ae, specializing the common almost-everywhere bound to the chosen event. The complete proof is reconstructed from the existing component; its target module is not imported.

/- SamplingOptimisationGeometryBench public-dev reference.
   Reuses the existing project proof; retain LICENSE and NOTICE. -/
import AutoSamplingTheory.TechnicalLemmas.Probability.KernelTotalVariation

open MeasureTheory ProbabilityTheory Set Finset
open scoped ProbabilityTheory BigOperators

example
    {A B : Type*} [MeasurableSpace A] [MeasurableSpace B]
    (μ : Measure A) [IsProbabilityMeasure μ]
    (K L : Kernel A B) [IsMarkovKernel K] [IsMarkovKernel L]
    (ε : A → ℝ) (hε : Integrable ε μ)
    (hbound : ∀ᵐ x ∂μ, ∀ s, MeasurableSet s →
      |(K x).real s - (L x).real s| ≤ ε x) :
    ∀ t, MeasurableSet t →
      |(K ∘ₘ μ).real t - (L ∘ₘ μ).real t| ≤ ∫ x, ε x ∂μ := by
  intro t ht
  have hint (M : Kernel A B) [IsMarkovKernel M] :
      Integrable (fun x => (M x).real t) μ := by
    apply (integrable_const (1 : ℝ)).mono'
      (M.measurable_coe ht).ennreal_toReal.aestronglyMeasurable
    exact Filter.Eventually.of_forall fun x => by
      rw [Real.norm_eq_abs, abs_of_nonneg ENNReal.toReal_nonneg]
      exact (measureReal_le_one : (M x).real t ≤ 1)
  have happly (M : Kernel A B) [IsMarkovKernel M] :
      (M ∘ₘ μ).real t = ∫ x, (M x).real t ∂μ := by
    change (Measure.bind μ M t).toReal = ∫ x, (M x t).toReal ∂μ
    rw [Measure.bind_apply ht M.aemeasurable]
    exact (integral_toReal (M.measurable_coe ht).aemeasurable
      (Filter.Eventually.of_forall fun x => measure_lt_top (M x) t)).symm
  rw [happly K, happly L, ← integral_sub (hint K) (hint L)]
  exact abs_integral_le_integral_abs.trans <|
    integral_mono_ae ((hint K).sub (hint L)).abs hε <|
      hbound.mono fun x hx => hx t ht

Download runnable reference