Well-conditioned RGO update: finite variance and contraction
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.RecursiveVariance.variance_update_bounds · theorem · Teaching coverage
Statement
For real r,h,c assume r≥0 and 0<h≤c. Define a=(h+c)/(1+r), the updated precision r⁺=r+a⁻¹, the updated regularization variance A⁺=(r⁺)⁻¹, and ρ=2c/(1+2c). Then r⁺>0, 0<A⁺≤2c and 0<ρ<1. Whenever r>0, A⁺≤ρ/r. No previous real variance is assigned to r=0: it represents the source's infinite initial parameter.
All objects and hypotheses
- r≥0 is precision. A previous finite regularization variance equals 1/r only when r>0; r=0 models A=∞ without using Lean's real inverse of zero as infinity.
- 0<h≤c implies c>0. The source restriction c<1/4 is not needed for this selected scalar branch.
- The well-conditioned branch has already selected τ=c. This theorem does not test its condition number, prove branch persistence or implement a recursive sampler.
- All quantities here are real scalar parameters, not random variables or the covariance of the Gibbs distribution. No measure-theoretic hypothesis is needed for the scalar inequalities.
Mathematical proof
1. Establish positivity before using reciprocals
Put t=h+c and β=1+r. The assumptions give 0<t≤2c and β≥1. Thus a=t/β is positive, and adding its positive inverse to nonnegative precision produces r⁺>0. Its inverse is consequently a genuine finite positive parameter.
Corresponding Lean step
hc, ht, ht_upper and hbeta establish these inequalities. div_pos, inv_pos and add_pos_of_nonneg_of_pos justify every inverse; positivity closes elementary sign obligations.
2. Write the updated variance in a uniform form
Substitute a and clear the positive denominator t. The expression D=1+r+rt is at least one, so the formula also holds at r=0. At that boundary it yields A⁺=t=h+c, handling the source's infinite initial variance without finite-A division.
Corresponding Lean step
hD proves denominator positivity. hformula uses inv_div and field_simp, then add_comm, to verify the identity. The focused zero-precision test checks a=Aplus=h+c, positivity and the bound.
3. Bound the first finite parameter
Since D≥1 and t>0, division by D cannot increase t. Combining this with the schedule bound proves A⁺≤2c even when the previous parameter was infinite.
Corresponding Lean step
hbound first applies le_trans and div_le_iff₀ hD. nlinarith checks the polynomial inequality using nonnegative products, with no extra analytic premise.
4. Prove a guarded finite-parameter contraction
Both D and 1+2c are positive. After multiplying by them, the desired bound rA⁺≤ρ reduces to the nonnegative residual 2c+r(2c−t). Also 2c is positive and strictly below 1+2c, so 0<ρ<1. Only when r>0 may we divide the scaled inequality by r to compare with the previous finite variance.
Corresponding Lean step
hscaled uses div_le_div_iff₀ and the nonnegativity of r(2c−t). div_lt_one proves ρ<1. The final implication explicitly introduces hrpos before le_div_iff₀ is used; real 0⁻¹ never becomes a previous variance.
Lean statement · variance_update_bounds
The let-bindings preserve the update without adding wrapper definitions. All parameters are real, and three explicit inequalities suffice. The strict r>0 hypothesis is confined to the final implication; the finite updated bound covers r=0 too.
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 variance_update_bounds {r h c : ℝ} (hr : 0 ≤ r) (hh : 0 < h)
(hhc : h ≤ c) :
let a := (h + c) / (1 + r)
let rp := r + a⁻¹
let Aplus := rp⁻¹
let rho := 2 * c / (1 + 2 * c)
0 < rp ∧ 0 < Aplus ∧ Aplus ≤ 2 * c ∧
0 < rho ∧ rho < 1 ∧ (0 < r → Aplus ≤ rho * r⁻¹)Lean proof · variance_update_bounds
Only Mathlib ordered-field facts and arithmetic tactics are imported. The production proof has no ASTIS dependency. A separate consumer test uses the same a,r⁺ and center in RGOCalculus.rgo_calculus, deriving an actual normalized updated Gibbs probability together with these inequalities, with no normalizer or probability premise.
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 variance_update_bounds {r h c : ℝ} (hr : 0 ≤ r) (hh : 0 < h)
(hhc : h ≤ c) :
let a := (h + c) / (1 + r)
let rp := r + a⁻¹
let Aplus := rp⁻¹
let rho := 2 * c / (1 + 2 * c)
0 < rp ∧ 0 < Aplus ∧ Aplus ≤ 2 * c ∧
0 < rho ∧ rho < 1 ∧ (0 < r → Aplus ≤ rho * r⁻¹) := by
have hc : 0 < c := lt_of_lt_of_le hh hhc
have ht : 0 < h + c := add_pos hh hc
have ht_upper : h + c ≤ 2 * c := by linarith
have hbeta : 0 < 1 + r := by positivity
have ha : 0 < (h + c) / (1 + r) := div_pos ht hbeta
have hrp : 0 < r + ((h + c) / (1 + r))⁻¹ :=
add_pos_of_nonneg_of_pos hr (inv_pos.mpr ha)
have hD : 0 < 1 + r + r * (h + c) := by positivity
have hformula :
(r + ((h + c) / (1 + r))⁻¹)⁻¹ =
(h + c) / (1 + r + r * (h + c)) := by
rw [inv_div]
field_simp
exact add_comm _ _
have hbound : (h + c) / (1 + r + r * (h + c)) ≤ 2 * c := by
apply le_trans _ ht_upper
apply (div_le_iff₀ hD).2
nlinarith [mul_nonneg hr ht.le, mul_nonneg ht.le (mul_nonneg hr ht.le)]
have hrhoden : 0 < 1 + 2 * c := by positivity
have hscaled : r * ((h + c) / (1 + r + r * (h + c))) ≤
2 * c / (1 + 2 * c) := by
rw [← mul_div_assoc]
apply (div_le_div_iff₀ hD hrhoden).2
nlinarith [mul_nonneg hr (sub_nonneg.mpr ht_upper)]
refine ⟨hrp, inv_pos.mpr hrp, ?_, div_pos (by positivity) hrhoden, ?_, ?_⟩
· simpa only [hformula] using hbound
· exact (div_lt_one hrhoden).2 (by linarith)
· intro hrpos
rw [hformula, ← div_eq_mul_inv]
apply (le_div_iff₀ hrpos).2
simpa only [mul_comm] using hscaled
end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.RecursiveVarianceScope and omitted-condition boundaries
- Only the deterministic well-conditioned parameter step of Lemma6.6(ii). The source condition-number test selects tau=c; it is not asserted by this lemma. c<1/4 is unnecessary for this scalar branch and explicitly generalized away. r^-1 represents a previous finite variance only under r>0. No finite-stage termination, implemented recursion, probability error, mixing or query cost.
- One-step regularization-parameter control is not a covariance estimate, a termination theorem, an error guarantee or an expected query-cost estimate.
Source and reuse
ASTIS parents called
Mathlib API called (external library)
- inv_div
- div_pos
- inv_pos
- div_le_iff₀
- div_le_div_iff₀
- div_lt_one
- le_div_iff₀
Mathematical sources
- Fan Chen, Sinho Chewi, Jianfeng Lu and Matthew S. Zhang, SPHMC v1, §6.3, Lemma 6.6(ii), (6.1)–(6.2) — ASTIS mathematical restatement and expanded scalar derivation; no verbatim paper proof reproduced.
- Mathlib contributors, Apache-2.0 — Reused ordered-field inequalities, not counted as newly formalized ASTIS leaves.
ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.