Why an ill-conditioned recursive stage makes geometric progress
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.RecursiveCondition.contraction_bounds · theorem · Teaching coverage
Mathematical statement
For any real numbers k and h with k at least 2 and h strictly between 0 and 1/4, the displayed rational update lies between k/2 and four fifths of k.
Lean statement · contraction_bounds
The parameters in braces are implicit real numbers; hk, hh and hh_upper are explicit hypotheses. The conjunction returns both inequalities. No typeclass or unproved sampler property is hidden in the statement.
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 contraction_bounds {k h : ℝ} (hk : 2 ≤ k) (hh : 0 < h)
(hh_upper : h < 1 / 4) :
k / 2 ≤ k * (k + h + 1) / (2 * k + h) ∧
k * (k + h + 1) / (2 * k + h) ≤ (4 / 5) * kProof roadmap
- 1Check division is legitimate
The denominator is positive. Thus multiplying either inequality by it preserves its direction; Lean's exceptional value for division by zero is irrelevant.
- 2Prove the lower bound
Subtract half the previous value. The numerator is nonnegative because both k and h are nonnegative.
- 3Prove the uniform contraction
The deficit from four fifths has a positive margin throughout the parameter range. This checks the paper's constants without an unspecified further reduction of c0.
Full assumptions and notation
All objects and hypotheses
- k,h are real scalars; 2 ≤ k and 0 < h < 1/4.
- In the paper application k is the ratio of the specified curvature bounds, h is the smoothing parameter, and tau=k. It is not necessarily the optimal condition number of the target.
- The source assumes 0<h≤c0<1/4. For this uniform single-stage calculation, eliminating the unused cutoff gives exactly 0<h<1/4; conversely any such h admits c0=h. No zero-smoothing or closed-endpoint extension is asserted.
- This calculation does not involve a measure, derivative or random variable. The recurrence-to-RGO identification is a separate obligation.
Mathematical proof
1. Check division is legitimate
The denominator is positive. Thus multiplying either inequality by it preserves its direction; Lean's exceptional value for division by zero is irrelevant.
Corresponding Lean step
hden proves strict positivity; le_div_iff₀ and div_le_iff₀ remove the denominator only after this proof.
2. Prove the lower bound
Subtract half the previous value. The numerator is nonnegative because both k and h are nonnegative.
Corresponding Lean step
The first branch uses mul_nonneg hk_nonneg hh.le, then nlinarith checks the cleared-denominator polynomial inequality.
3. Prove the uniform contraction
The deficit from four fifths has a positive margin throughout the parameter range. This checks the paper's constants without an unspecified further reduction of c0.
Corresponding Lean step
hmargin proves 0 ≤ 3*k-h-5 by linarith. Its product with k is nonnegative; nlinarith closes the upper bound.
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · contraction_bounds
constructor separates the two inequalities. Positivity licenses cross-multiplication; mul_nonneg supplies the needed products; linarith and nlinarith generate checked ordered-field proofs. ASTIS authors this source-specific recurrence estimate; Mathlib supplies real arithmetic and the proof-producing tactics.
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 contraction_bounds {k h : ℝ} (hk : 2 ≤ k) (hh : 0 < h)
(hh_upper : h < 1 / 4) :
k / 2 ≤ k * (k + h + 1) / (2 * k + h) ∧
k * (k + h + 1) / (2 * k + h) ≤ (4 / 5) * k := by
have hk_nonneg : 0 ≤ k := by linarith
have hden : 0 < 2 * k + h := by linarith
constructor
· apply (le_div_iff₀ hden).2
nlinarith [mul_nonneg hk_nonneg hh.le]
· apply (div_le_iff₀ hden).2
have hmargin : 0 ≤ 3 * k - h - 5 := by linarith
nlinarith [mul_nonneg hk_nonneg hmargin]
end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.RecursiveConditionSource assumptions versus formal assumptions
| Source | Actual Lean | Difference kind | Why it matters |
|---|---|---|---|
| 0<eta≤c0<1/4 | 0<h<1/4 | same | For the uniform single-stage scalar assertion c0 occurs only in the hypotheses. The source implies this range; conversely an admissible c0 exists, for example c0=h. This eliminates a redundant cutoff without adding endpoints. |
| kappa_j is the ratio from the actual RGO parameter recurrence | k is a real scalar at least 2, with the rational update written explicitly | unresolved | This leaf proves the arithmetic proof step. The actual RGO construction and curvature-to-recurrence identification remain a separate red edge. |
Scalar proof component, not the RGO parameter construction or the complete sampling theorem.
Encoder–denoiser: accepted · equivalent-after-elaboration
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
- Only Lemma 6.6(i)'s scalar calculation is covered. Lemma 6.4's normalized RGO closure and curvature formulas remain separate.
- The well-conditioned phase, finite termination, sampling-error propagation and actual expected query count are not conclusions.
- The first test checks k=2,h=1/8; the second derives this interface from the paper's strict c0 range. An earlier unneeded endpoint generalization was removed after independent source review; its artifacts are retained.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
Mathlib API called (external library)
- le_div_iff₀ and div_le_iff₀: ordered-field division with a strictly positive denominator.
- mul_nonneg: nonnegative products; Mathlib linarith/nlinarith: kernel-checked polynomial arithmetic.
Mathematical sources
- Chen, Chewi, Lu and Zhang, Smoothed Picard Hamiltonian Monte Carlo v1 — Lemma 6.6(i), (6.3), after substituting (6.1) and (6.2). ASTIS exposition, not quoted prose.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.