Samplinglib mathematical lesson

Average a history-dependent one-call kernel error

AutoSamplingTheory.TechnicalLemmas.Probability.KernelHybridTelescope.abs_real_comp_sub_le_integral_eventBound · theorem · Teaching coverage

Read this first

Mathematical statement

Let μ be a probability law on a measurable history space A, let K and L be Markov kernels from A to an output space B, and let ε:A→ℝ be μ-integrable. If, for μ-almost every history x, every measurable output event S satisfies |K(x,S)−L(x,S)|≤ε(x), then every measurable T satisfies |(μK)(T)−(μL)(T)|≤∫ε dμ.

\[\left|(\mu K)(T)-(\mu L)(T)\right|\le \int_A\varepsilon(x)\,\mu(dx),\qquad \left|K(x,S)-L(x,S)\right|\le\varepsilon(x).\]

Lean statement · abs_real_comp_sub_le_integral_eventBound

Lean writes K ∘ₘ μ for the measure obtained by first drawing x∼μ and then drawing from K(x,·). The theorem works eventwise and deliberately uses no competing total-variation definition.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

Download module (.lean)

theorem abs_real_comp_sub_le_integral_eventBound
    {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 ∂μ

Exact module and namespace context

Proof roadmap

1Write both output probabilities as history integrals
Fix a measurable output event T. Kernel measurability makes x↦K(x,T) and x↦L(x,T) measurable, and the Markov property bounds both functions between zero and one. They are therefore integrable under the probability law μ. The definition of passing μ through a kernel gives ordinary real integrals.
2Move subtraction inside the integral
Because both conditional event-probability functions are integrable, their integral difference equals the integral of their pointwise difference. This is the hidden condition behind the paper-level instruction to average the conditional error.
3Use the conditional budget under the ideal history law
The absolute value of an integral is at most the integral of the absolute value. Specializing the almost-everywhere hypothesis to T then bounds the integrand by ε(x), and monotonicity of the integral yields the claimed mean error. The result retains the expected local budget; it does not replace it by a worst-case bound.

Full assumptions and notation

All objects and hypotheses

A and B carry measurable spaces; μ is a probability measure and K,L are genuine Markov probability kernels.
The conditional event bound holds μ-almost everywhere and uniformly over every measurable event S at each accepted history.
ε is a real-valued μ-integrable function. The event bound itself forces ε≥0 on the histories where it holds; no separate nonnegativity premise is needed.
All event masses are finite probabilities, so conversion from extended nonnegative values to real values loses no information.

Mathematical proof

1. Write both output probabilities as history integrals

Fix a measurable output event T. Kernel measurability makes x↦K(x,T) and x↦L(x,T) measurable, and the Markov property bounds both functions between zero and one. They are therefore integrable under the probability law μ. The definition of passing μ through a kernel gives ordinary real integrals.

\[(\mu K)(T)=\int_A K(x,T)\,\mu(dx),\qquad (\mu L)(T)=\int_A L(x,T)\,\mu(dx).\]

Corresponding Lean step

The local hint proves integrability from Kernel.measurable_coe and measureReal_le_one. The local happly unfolds Measure.bind, uses Measure.bind_apply, and invokes integral_toReal after proving every conditional event has finite mass.

2. Move subtraction inside the integral

Because both conditional event-probability functions are integrable, their integral difference equals the integral of their pointwise difference. This is the hidden condition behind the paper-level instruction to average the conditional error.

\[(\mu K)(T)-(\mu L)(T)=\int_A\bigl(K(x,T)-L(x,T)\bigr)\,\mu(dx).\]

Corresponding Lean step

integral_sub is applied only after hint K and hint L have supplied both integrability witnesses.

3. Use the conditional budget under the ideal history law

The absolute value of an integral is at most the integral of the absolute value. Specializing the almost-everywhere hypothesis to T then bounds the integrand by ε(x), and monotonicity of the integral yields the claimed mean error. The result retains the expected local budget; it does not replace it by a worst-case bound.

\[\left|\int_A(K(x,T)-L(x,T))\,d\mu\right|\le\int_A|K(x,T)-L(x,T)|\,d\mu\le\int_A\varepsilon(x)\,d\mu.\]

Corresponding Lean step

abs_integral_le_integral_abs supplies the first inequality. Integrable.abs and integral_mono_ae use hbound specialized to T for the second.

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · abs_real_comp_sub_le_integral_eventBound

The proof establishes bounded conditional-event integrability, expands both kernel compositions, subtracts the two integrals, and applies the pointwise conditional budget almost everywhere.

Download module (.lean)

theorem abs_real_comp_sub_le_integral_eventBound
    {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

Exact module and namespace context

Scope and omitted-condition boundaries

This is the mean one-call replacement edge in Lemma 6.3, not the full adaptive hybrid theorem.
It does not construct the Gaussian-cloud history law, show that a local implementation has the stated conditional TV error, or prove measurability of a supremum-defined TV function.
It does not add the capped-versus-uncapped error ε_cap.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Kernel.measurable_coe
Measure.bind_apply
integral_toReal
integral_sub
abs_integral_le_integral_abs
integral_mono_ae

Mathematical sources

Chen, Chewi, Lu and Zhang, Gaussian cloud correction v1, Section 6.1, Lemma 6.3 — ASTIS expansion of the conditional mean-error step; no paper prose is reproduced.

Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.