Finite adjacent hybrid errors add
AutoSamplingTheory.TechnicalLemmas.Probability.KernelHybridTelescope.abs_sub_zero_le_sum_range_of_adjacent · theorem · Teaching coverage
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.
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, δ iProof 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.
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.
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.KernelHybridTelescopeScope 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.