KernelHybridTelescope: mathematical reading route

Read the statements and derivations in source order. Every result has its own optional Lean statement and proof. Source assumptions, library reuse and unproved boundaries are kept explicit.

Average a history-dependent one-call kernel error
Later adaptive computation cannot amplify one replaced call
Finite adjacent hybrid errors add

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.

Samplinglib mathematical lesson

Later adaptive computation cannot amplify one replaced call

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

Read this first

Mathematical statement

Under the preceding hypotheses, let S be any Markov kernel from the one-call output space B to a final output space C. Applying the same downstream kernel S after K and after L preserves the mean error bound: every measurable final event T differs by at most ∫ε dμ.

\[\left|\bigl(\mu(KS)\bigr)(T)-\bigl(\mu(LS)\bigr)(T)\right|\le\int_A\varepsilon\,d\mu.\]

Lean statement · abs_real_comp_commonSuffix_sub_le_integral_eventBound

The theorem is generic over three measurable spaces. The common-suffix condition is visible in the single parameter S rather than hidden in prose about continuing the algorithm.

Download module (.lean)

theorem abs_real_comp_commonSuffix_sub_le_integral_eventBound
    {A B C : Type*} [MeasurableSpace A] [MeasurableSpace B] [MeasurableSpace C]
    (μ : Measure A) [IsProbabilityMeasure μ]
    (K L : Kernel A B) [IsMarkovKernel K] [IsMarkovKernel L]
    (S : Kernel B C) [IsMarkovKernel S]
    (ε : A → ℝ) (hε : Integrable ε μ)
    (hbound : ∀ᵐ x ∂μ, ∀ s, MeasurableSet s →
      |(K x).real s - (L x).real s| ≤ ε x) :
    ∀ t, MeasurableSet t →
      |((S ∘ₖ K) ∘ₘ μ).real t - ((S ∘ₖ L) ∘ₘ μ).real t| ≤
        ∫ x, ε x ∂μ

Exact module and namespace context

Proof roadmap

1Control the laws immediately after the replaced slot
The first theorem gives an eventwise discrepancy bound between μK and μL equal to the ideal-history mean of the local budget.
2Apply total-variation data processing to the common suffix
A common Markov kernel cannot increase an eventwise total-variation bound. Treat every later adaptive action, including its final readout, as S. This is the mathematical reason adjacent hybrids only pay for the slot at which they differ.

Full assumptions and notation

All objects and hypotheses

The input law, two replacement kernels and conditional error budget satisfy the first theorem.
S is the same Markov kernel in both hybrids. In an adaptive proof, the history state must contain enough information that all later calls really are represented by this common suffix.
Kernel associativity is used as equality of composed measures; no informal reassociation of conditional distributions is assumed.

Mathematical proof

1. Control the laws immediately after the replaced slot

The first theorem gives an eventwise discrepancy bound between μK and μL equal to the ideal-history mean of the local budget.

\[\forall U,\quad |(\mu K)(U)-(\mu L)(U)|\le\int_A\varepsilon\,d\mu.\]

Corresponding Lean step

abs_real_comp_sub_le_integral_eventBound is called with exactly the same μ,K,L,ε and almost-everywhere conditional estimate.

2. Apply total-variation data processing to the common suffix

A common Markov kernel cannot increase an eventwise total-variation bound. Treat every later adaptive action, including its final readout, as S. This is the mathematical reason adjacent hybrids only pay for the slot at which they differ.

\[\sup_T|((\mu K)S)(T)-((\mu L)S)(T)|\le\sup_U|(\mu K)(U)-(\mu L)(U)|.\]

Corresponding Lean step

KernelTotalVariation.abs_real_comp_sub_le supplies factor-one contraction. Measure.comp_assoc rewrites the result into the source-facing composition order.

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_commonSuffix_sub_le_integral_eventBound

First obtain the mean discrepancy of the intermediate laws; then reuse the compiled ASTIS Markov-kernel contraction theorem and associativity.

Download module (.lean)

theorem abs_real_comp_commonSuffix_sub_le_integral_eventBound
    {A B C : Type*} [MeasurableSpace A] [MeasurableSpace B] [MeasurableSpace C]
    (μ : Measure A) [IsProbabilityMeasure μ]
    (K L : Kernel A B) [IsMarkovKernel K] [IsMarkovKernel L]
    (S : Kernel B C) [IsMarkovKernel S]
    (ε : A → ℝ) (hε : Integrable ε μ)
    (hbound : ∀ᵐ x ∂μ, ∀ s, MeasurableSet s →
      |(K x).real s - (L x).real s| ≤ ε x) :
    ∀ t, MeasurableSet t →
      |((S ∘ₖ K) ∘ₘ μ).real t - ((S ∘ₖ L) ∘ₘ μ).real t| ≤
        ∫ x, ε x ∂μ := by
  have hKL := abs_real_comp_sub_le_integral_eventBound μ K L ε hε hbound
  have hS := KernelTotalVariation.abs_real_comp_sub_le
    (K ∘ₘ μ) (L ∘ₘ μ) S hKL
  simpa only [← Measure.comp_assoc] using hS

Exact module and namespace context

Scope and omitted-condition boundaries

A source adapter must still construct the dummy-filled history state and prove that the suffix is common after one slot is replaced.
Different later kernels, stopping rules not encoded in the state, or uncapped recursion are not covered.
No Gaussian-cloud-specific local accuracy estimate is proved here.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Measure.comp_assoc

Mathematical sources

Chen, Chewi, Lu and Zhang, Gaussian cloud correction v1, Lemma 6.3 hybrid proof — Formal data-processing core for the adjacent-hybrid suffix.

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

Samplinglib mathematical lesson

Finite adjacent hybrid errors add

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

Read this first

Mathematical statement

For real sequences a and δ and a natural number n, if every adjacent difference |a(i+1)−a(i)| is at most δ(i) for i<n, then the endpoint difference |a(n)−a(0)| is at most the sum of those n budgets.

\[\bigl|a_n-a_0\bigr|\le\sum_{i=0}^{n-1}\delta_i\quad\text{whenever}\quad |a_{i+1}-a_i|\le\delta_i.\]

Lean statement · abs_sub_zero_le_sum_range_of_adjacent

This small real theorem is intentionally separate from probability-kernel definitions: it can telescope event discrepancies produced by any adjacent-hybrid construction without inventing another total-variation object.

Download module (.lean)

theorem abs_sub_zero_le_sum_range_of_adjacent
    (a δ : ℕ → ℝ) (n : ℕ)
    (hstep : ∀ i < n, |a (i + 1) - a i| ≤ δ i) :
    |a n - a 0| ≤ ∑ i ∈ range n, δ i

Exact module and namespace context

Proof roadmap

1Split the last endpoint difference
Insert the penultimate value a_n between a_{n+1} and a_0. The real triangle inequality separates the newest replacement error from the accumulated earlier error.
2Apply the newest budget and the induction hypothesis
The step assumption bounds the first term by δ_n. The induction hypothesis bounds the second by the sum through n−1. Appending δ_n gives exactly the finite range sum through n.

Full assumptions and notation

All objects and hypotheses

The hybrid chain has a fixed finite length n; this theorem says nothing about a random or infinite number of calls.
Each adjacent discrepancy is a real number with the displayed bound. In the paper consumer, a_i is the probability of one fixed output event under hybrid i.
The same event is followed through the whole telescope before taking a total-variation supremum.

Mathematical proof

1. Split the last endpoint difference

Insert the penultimate value a_n between a_{n+1} and a_0. The real triangle inequality separates the newest replacement error from the accumulated earlier error.

\[|a_{n+1}-a_0|\le|a_{n+1}-a_n|+|a_n-a_0|.\]

Corresponding Lean step

abs_sub_le is the triangle inequality in the required three-point form.

2. Apply the newest budget and the induction hypothesis

The step assumption bounds the first term by δ_n. The induction hypothesis bounds the second by the sum through n−1. Appending δ_n gives exactly the finite range sum through n.

\[|a_{n+1}-a_0|\le\delta_n+\sum_{i=0}^{n-1}\delta_i=\sum_{i=0}^{n}\delta_i.\]

Corresponding Lean step

add_le_add combines the two bounds; Finset.sum_range_succ and commutativity identify the resulting expression with the canonical range sum.

Lean verification

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

Lean proof · abs_sub_zero_le_sum_range_of_adjacent

Induction on n, one application of the three-point absolute-value inequality, and the finite range-sum recursion.

Download module (.lean)

theorem abs_sub_zero_le_sum_range_of_adjacent
    (a δ : ℕ → ℝ) (n : ℕ)
    (hstep : ∀ i < n, |a (i + 1) - a i| ≤ δ i) :
    |a n - a 0| ≤ ∑ i ∈ range n, δ i := by
  induction n with
  | zero => simp
  | succ n ih =>
      calc
        |a (n + 1) - a 0| ≤ |a (n + 1) - a n| + |a n - a 0| := by
          exact abs_sub_le _ _ _
        _ ≤ δ n + ∑ i ∈ range n, δ i :=
          add_le_add (hstep n (Nat.lt_succ_self n))
            (ih fun i hi => hstep i (hi.trans (Nat.lt_succ_self n)))
        _ = ∑ i ∈ range (n + 1), δ i := by
          rw [sum_range_succ, add_comm]

end AutoSamplingTheory.TechnicalLemmas.Probability.KernelHybridTelescope

Exact module and namespace context

Scope and omitted-condition boundaries

This theorem does not produce the adjacent kernel inequalities; the preceding two declarations do that after a suitable history-space construction.
It does not prove the source paper's stopping-time tail, deterministic cap, or ε_cap comparison.
Expected query complexity is independent of this deterministic error accumulation.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

abs_sub_le
Finset.sum_range_succ

Mathematical sources

Chen, Chewi, Lu and Zhang, Gaussian cloud correction v1, Lemma 6.3 — Finite triangle-telescope used after adjacent hybrid comparison.

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