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.

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_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.