The adaptive sampler and Lemma 6.3 are due to Fan Chen, Sinho Chewi, Jianfeng Lu and Matthew S. Zhang. The explicit measurable-kernel decomposition is ASTIS's rigorous supporting expansion; no author endorsement is implied.
For a capped adaptive algorithm represented on a common dummy-filled history space, replacing one conditional kernel at a time changes the final output law by at most the ideal-history expectation of that call's conditional total-variation error. Summing adjacent hybrids gives the total capped implementation error; a separate capped-versus-uncapped comparison contributes epsilon_cap exactly once.
Each statement and proof below has its own closed Lean disclosure. Samplinglib parents, Mathlib calls and external mathematical sources are distinguished in each proof.
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.
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.
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.
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
Source assumptions versus formal assumptions
Mean eventwise conditional error only; no history construction, TV-supremum measurability, dummy continuation or cap comparison.
Encoder–denoiser: accepted · equivalent-after-elaboration
Detected semantic differences
- scopes: The formal component uses an explicit integrable eventwise budget instead of constructing the paper's measurable conditional-TV function or identifying its expectation with delta_t. This is an explicitly deferred adapter, not a hidden completed source obligation. — Independent source review classification: explicit-elaboration; nonblocking.
- domains: The result is generic over measurable spaces and supplied kernels. Its source application requires a separate construction of the appropriate ideal-history law and transition kernels. — Independent source review classification: documented-generalization; nonblocking.
A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.
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
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.
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.
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.
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.
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
Source assumptions versus formal assumptions
Common Markov suffix only; proving that the paper's later adaptive calls define this suffix is still open.
Encoder–denoiser: accepted · equivalent-after-elaboration
Detected semantic differences
- scopes: The informal shared adaptive continuation becomes an explicit single Markov kernel S. Constructing that kernel on a sufficiently rich retained-history state remains a separate source adapter, as the packet expressly states. — Independent source review classification: explicit-elaboration; nonblocking.
- conclusion: This component preserves a supplied conditional eventwise budget; it neither identifies the paper's delta_t nor certifies the full dummy-history, cap or complexity argument. — Independent source review classification: scope-clarification; nonblocking.
A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.
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)
Mathematical sources
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.
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.
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.
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.
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
Source assumptions versus formal assumptions
Finite real triangle telescope only; dummy histories, conditional kernel bounds and epsilon_cap remain separate.
Encoder–denoiser: accepted · equivalent-after-elaboration
Detected semantic differences
- domains: The formal telescope works for arbitrary real sequences, not just event probabilities. Its source instance uses a(i)=P_i(T) for one fixed event T; the extra generality does not change the adjacent-bound argument. — Independent source review classification: documented-generalization; nonblocking.
- quantifiers: Formal indices zero through n-1 correspond to source call slots one through n. The result remains an eventwise finite telescope and does not itself take the total-variation supremum or add the cap-comparison error. — Independent source review classification: notation-resolution; nonblocking.
A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.
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
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.