Actual recursive schedule: persistent good conditioning and a terminal parameter bound
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.RecursiveDepth.parameter_control · theorem · Teaching coverage
Statement
For the normalized recursive RGO schedule assume κ≥1, r₀≥0, 0<c<1/4 and 0<ηⱼ≤c for every j. Define K(r)=(1+r)/(κ⁻¹+r), τ(r)=K(r) for K(r)≥2 and τ(r)=c otherwise, a(r,h)=(h+τ(r))/(1+r), and rⱼ₊₁=rⱼ+1/a(rⱼ,ηⱼ). All rⱼ are nonnegative and every rⱼ₊₁ is positive. K(rⱼ) is nonincreasing, so a stage below two stays below two at every later stage. If (4/5)^M K(r₀)<2, then for every N≥0, 0<1/r_(M+1+N)≤2c[2c/(1+2c)]^N. For every B>0, some J>0 satisfies 0<1/rⱼ≤B. These are the parameter consequences of Lemma6.4, the schedule and Lemma6.6 used in the terminal-stage argument; they do not claim the full recursive sampling theorem or its prescribed logarithmic constants.
All objects and hypotheses
- κ≥1, r₀≥0, 0<c<1/4, and every real ηⱼ satisfies 0<ηⱼ≤c. κ≥1 retains the original α≤β condition after normalization.
- K(r)=(1+r)/(κ⁻¹+r); τ(r)=K(r) if K(r)≥2 and c otherwise; a(r,h)=(h+τ(r))/(1+r); the sequence starts at r₀ and adds 1/a(rⱼ,ηⱼ) at each step. These are definitions, not supplied contraction hypotheses.
- All quantities in this theorem are deterministic real parameters and natural stage indices. η may be any admissible sequence; the result can be applied to a realized sequence but constructs no measurable random sequence.
- Zero initial precision represents infinite initial regularization. Only strictly positive successor precisions are interpreted as finite reciprocal variance. The parameter is not Gibbs covariance.
Mathematical proof
1. Positive precision and decreasing condition number
Set b=κ⁻¹. Then 0<b≤1. Every heat duration is positive; hence a>0 and r⁺>r≥0. The first successor has finite positive inverse even if r₀=0. For s≥r≥0, positive-denominator cross multiplication shows K(s)≤K(r), because the relevant residual is (s−r)(1−b)≥0. Induction gives nonnegative precisions and a nonincreasing condition sequence.
Corresponding Lean step
Local condition_bounds, condition_antitone and precision_nonneg establish signs; condition_sequence_antitone uses antitone_nat_of_succ_le. All helper facts are internal proof steps of the one published theorem.
2. Identify the actual large-branch update
For t=η+τ>0, substitute the precision update into K and clear positive denominators. In the branch K≥2, τ=K, so the existing large-branch scalar theorem bounds the actual next K by 4K/5. No contraction is assumed.
Corresponding Lean step
Local ratio_update verifies the rational identity. large_branch_contraction selects the actual if-branch and calls RecursiveCondition.contraction_bounds with 0<η≤c<1/4.
3. Reach and preserve the good regime
If the condition at stage M were at least two, monotonicity would force every earlier stage to remain in the large branch. The preceding contraction and the existing geometric-sequence lemma would contradict the strict certificate. The condition then remains below two for all later indices, so every later heat duration equals c.
Corresponding Lean step
enters_well_conditioned uses le_geom under the contradiction hypothesis; well_conditioned_persists applies the proved antitone relation. Equality K=2 is kept in the large branch.
4. Start with one genuinely finite parameter
Apply the existing small-branch variance bound at stage M. It yields a positive A_(M+1)≤2c, including when M=0 and r₀=0. The guaranteed finite starting stage for this geometric certificate is M+1; earlier stages may also have finite parameters.
Corresponding Lean step
well_branch_variance unfolds the actual c branch and calls RecursiveVariance.variance_update_bounds. The consumer test checks κ=1, r₀=0, η=c=1/8 and arbitrary subsequent N.
5. Propagate the exact geometric bound
Every later precision is positive, so the guarded reciprocal contraction is applicable. Inducting N times after the first finite stage gives A_(M+1+N)≤2cρ^N. Every such reciprocal is positive.
Corresponding Lean step
The local finite_depth proof uses successor positivity before each reciprocal comparison; its index conversion identifies M+1+(N+1) with (M+1+N)+1.
6. Reach an arbitrary positive threshold
Since K₀≥1 and ρ<1, geometric powers provide M with (4/5)^M<2/K₀ and N with ρ^N<B/(2c). The preceding bound at J=M+1+N proves the threshold statement. This is an explicit geometric certificate and existential termination, not the source logarithmic-depth complexity bound.
Corresponding Lean step
exists_pow_lt_of_lt_one supplies both natural indices. The final local exists_terminal fact is combined with positivity, monotonicity, persistence and finite_depth in parameter_control.
Lean statement · parameter_control
Five local let-definitions expose the exact source schedule and Nat.rec evolution. The conclusion bundles positive precisions, antitone condition numbers, persistent strict good conditioning, the M+1+N geometric bound, and existence of a positive terminal stage.
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 parameter_control {κ c r₀ : ℝ} {η : ℕ → ℝ}
(hκ : 1 ≤ κ) (hc : 0 < c) (hc_upper : c < 1 / 4) (hr₀ : 0 ≤ r₀)
(hη : ∀ n, 0 < η n ∧ η n ≤ c) :
let K := fun r : ℝ => (1 + r) / (κ⁻¹ + r)
let τ := fun r : ℝ => if 2 ≤ K r then K r else c
let a := fun r h : ℝ => (h + τ r) / (1 + r)
let step := fun r h : ℝ => r + (a r h)⁻¹
let r : ℕ → ℝ := Nat.rec r₀ (fun j r => step r (η j))
(∀ n, 0 ≤ r n ∧ 0 < r (n + 1)) ∧
Antitone (fun n => K (r n)) ∧
(∀ m n, m ≤ n → K (r m) < 2 → K (r n) < 2) ∧
(∀ M N, (4 / 5 : ℝ)^M * K r₀ < 2 →
0 < (r (M + 1 + N))⁻¹ ∧
(r (M + 1 + N))⁻¹ ≤ 2 * c * (2 * c / (1 + 2 * c))^N) ∧
(∀ B : ℝ, 0 < B → ∃ J : ℕ,
0 < J ∧ 0 < (r J)⁻¹ ∧ (r J)⁻¹ ≤ B)Lean proof · parameter_control
The former helper calculations are local have proofs, not extra public theorem claims. The two existing scalar contraction theorems and Mathlib geometric-power facts are actual proof dependencies. A separate Gibbs consumer uses the same parameters with RGOCalculus.rgo_calculus; this proves next-target probability only.
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 parameter_control {κ c r₀ : ℝ} {η : ℕ → ℝ}
(hκ : 1 ≤ κ) (hc : 0 < c) (hc_upper : c < 1 / 4) (hr₀ : 0 ≤ r₀)
(hη : ∀ n, 0 < η n ∧ η n ≤ c) :
let K := fun r : ℝ => (1 + r) / (κ⁻¹ + r)
let τ := fun r : ℝ => if 2 ≤ K r then K r else c
let a := fun r h : ℝ => (h + τ r) / (1 + r)
let step := fun r h : ℝ => r + (a r h)⁻¹
let r : ℕ → ℝ := Nat.rec r₀ (fun j r => step r (η j))
(∀ n, 0 ≤ r n ∧ 0 < r (n + 1)) ∧
Antitone (fun n => K (r n)) ∧
(∀ m n, m ≤ n → K (r m) < 2 → K (r n) < 2) ∧
(∀ M N, (4 / 5 : ℝ)^M * K r₀ < 2 →
0 < (r (M + 1 + N))⁻¹ ∧
(r (M + 1 + N))⁻¹ ≤ 2 * c * (2 * c / (1 + 2 * c))^N) ∧
(∀ B : ℝ, 0 < B → ∃ J : ℕ,
0 < J ∧ 0 < (r J)⁻¹ ∧ (r J)⁻¹ ≤ B) := by
let condition (κ r : ℝ) : ℝ := (1 + r) / (κ⁻¹ + r)
let heat (κ c r : ℝ) : ℝ := if 2 ≤ condition κ r then condition κ r else c
let stepVariance (κ c r h : ℝ) : ℝ := (h + heat κ c r) / (1 + r)
let nextPrecision (κ c r h : ℝ) : ℝ := r + (stepVariance κ c r h)⁻¹
let precision (κ c r₀ : ℝ) (η : ℕ → ℝ) : ℕ → ℝ :=
Nat.rec r₀ (fun j r => nextPrecision κ c r (η j))
have condition_bounds {κ r : ℝ} (hκ : 1 ≤ κ) (hr : 0 ≤ r) :
1 ≤ condition κ r := by
have hkpos : 0 < κ := lt_of_lt_of_le zero_lt_one hκ
have hbpos : 0 < κ⁻¹ := inv_pos.mpr hkpos
have hble : κ⁻¹ ≤ 1 := (inv_le_one₀ hkpos).2 hκ
unfold condition
apply (one_le_div (add_pos_of_pos_of_nonneg hbpos hr)).2
linarith
have condition_antitone {κ r s : ℝ} (hκ : 1 ≤ κ)
(hr : 0 ≤ r) (hrs : r ≤ s) : condition κ s ≤ condition κ r := by
have hkpos : 0 < κ := lt_of_lt_of_le zero_lt_one hκ
have hbpos : 0 < κ⁻¹ := inv_pos.mpr hkpos
have hble : κ⁻¹ ≤ 1 := (inv_le_one₀ hkpos).2 hκ
unfold condition
apply (div_le_div_iff₀ (add_pos_of_pos_of_nonneg hbpos (hr.trans hrs))
(add_pos_of_pos_of_nonneg hbpos hr)).2
nlinarith [mul_nonneg (sub_nonneg.mpr hrs) (sub_nonneg.mpr hble)]
have stepVariance_pos {κ c r h : ℝ} (_hκ : 1 ≤ κ)
(hc : 0 < c) (hr : 0 ≤ r) (hh : 0 < h) :
0 < stepVariance κ c r h := by
have hheat : 0 < heat κ c r := by
unfold heat
split_ifs with hk
· linarith
· exact hc
exact div_pos (add_pos hh hheat) (by linarith)
have nextPrecision_gt {κ c r h : ℝ} (hκ : 1 ≤ κ)
(hc : 0 < c) (hr : 0 ≤ r) (hh : 0 < h) :
r < nextPrecision κ c r h := by
exact lt_add_of_pos_right r (inv_pos.mpr (stepVariance_pos hκ hc hr hh))
have precision_nonneg {κ c r₀ : ℝ} {η : ℕ → ℝ}
(hκ : 1 ≤ κ) (hc : 0 < c) (hr₀ : 0 ≤ r₀) (hη : ∀ n, 0 < η n)
(n : ℕ) : 0 ≤ precision κ c r₀ η n := by
induction n with
| zero => exact hr₀
| succ n ih =>
exact ih.trans (nextPrecision_gt hκ hc ih (hη n)).le
have precision_succ_pos {κ c r₀ : ℝ} {η : ℕ → ℝ}
(hκ : 1 ≤ κ) (hc : 0 < c) (hr₀ : 0 ≤ r₀) (hη : ∀ n, 0 < η n)
(n : ℕ) : 0 < precision κ c r₀ η (n + 1) := by
have hr := precision_nonneg hκ hc hr₀ hη n
exact lt_of_le_of_lt hr (nextPrecision_gt hκ hc hr (hη n))
have condition_sequence_antitone {κ c r₀ : ℝ} {η : ℕ → ℝ}
(hκ : 1 ≤ κ) (hc : 0 < c) (hr₀ : 0 ≤ r₀) (hη : ∀ n, 0 < η n) :
Antitone (fun n => condition κ (precision κ c r₀ η n)) := by
apply antitone_nat_of_succ_le
intro n
have hr := precision_nonneg hκ hc hr₀ hη n
exact condition_antitone hκ hr (nextPrecision_gt hκ hc hr (hη n)).le
have well_conditioned_persists {κ c r₀ : ℝ} {η : ℕ → ℝ}
(hκ : 1 ≤ κ) (hc : 0 < c) (hr₀ : 0 ≤ r₀) (hη : ∀ n, 0 < η n)
{m n : ℕ} (hmn : m ≤ n) (hm : condition κ (precision κ c r₀ η m) < 2) :
condition κ (precision κ c r₀ η n) < 2 :=
lt_of_le_of_lt (condition_sequence_antitone hκ hc hr₀ hη hmn) hm
have ratio_update {b r t : ℝ} (hb : 0 < b) (hr : 0 ≤ r)
(ht : 0 < t) :
(1 + (r + (t / (1 + r))⁻¹)) / (b + (r + (t / (1 + r))⁻¹)) =
((1 + r) / (b + r)) * (t + 1) / (t + (1 + r) / (b + r)) := by
have hB : 0 < 1 + r := by linarith
have hD : 0 < b + r := add_pos_of_pos_of_nonneg hb hr
have hnext : 0 < b + (r + (t / (1 + r))⁻¹) := by positivity
have hden : 0 < t + (1 + r) / (b + r) := by positivity
rw [inv_div]
field_simp
ring
have large_branch_contraction {κ c r h : ℝ}
(hκ : 1 ≤ κ) (hr : 0 ≤ r) (hh : 0 < h) (hhc : h ≤ c)
(hc : c < 1 / 4) (hk : 2 ≤ condition κ r) :
condition κ (nextPrecision κ c r h) ≤ (4 / 5) * condition κ r := by
have hkpos : 0 < κ := lt_of_lt_of_le zero_lt_one hκ
have ht : 0 < h + condition κ r := by linarith
have heq := ratio_update (inv_pos.mpr hkpos) hr ht
have hb := (RecursiveCondition.contraction_bounds hk hh (lt_of_le_of_lt hhc hc)).2
unfold nextPrecision stepVariance heat
rw [if_pos hk]
unfold condition at *
rw [heq]
convert hb using 1
congr 1 <;> ring
have enters_well_conditioned {κ c r₀ : ℝ} {η : ℕ → ℝ}
(hκ : 1 ≤ κ) (hc : 0 < c) (hc_upper : c < 1 / 4) (hr₀ : 0 ≤ r₀)
(hη : ∀ n, 0 < η n ∧ η n ≤ c) (M : ℕ)
(hM : (4 / 5 : ℝ) ^ M * condition κ r₀ < 2) :
condition κ (precision κ c r₀ η M) < 2 := by
by_contra hnot
have hlarge : 2 ≤ condition κ (precision κ c r₀ η M) := le_of_not_gt hnot
have hanti := condition_sequence_antitone hκ hc hr₀ (fun n => (hη n).1)
have hbound := le_geom (u := fun n => condition κ (precision κ c r₀ η n))
(c := (4 / 5 : ℝ)) (by norm_num) M (by
intro n hn
have hnlarge := hlarge.trans (hanti (Nat.le_of_lt hn))
exact large_branch_contraction hκ
(precision_nonneg hκ hc hr₀ (fun j => (hη j).1) n)
(hη n).1 (hη n).2 hc_upper hnlarge)
have : condition κ (precision κ c r₀ η M) < 2 := lt_of_le_of_lt hbound hM
exact (not_lt_of_ge hlarge) this
have well_branch_variance {κ c r h : ℝ} (hr : 0 ≤ r)
(hh : 0 < h) (hhc : h ≤ c) (hk : condition κ r < 2) :
0 < (nextPrecision κ c r h)⁻¹ ∧
(nextPrecision κ c r h)⁻¹ ≤ 2 * c ∧
(0 < r → (nextPrecision κ c r h)⁻¹ ≤ (2 * c / (1 + 2 * c)) * r⁻¹) := by
rcases RecursiveVariance.variance_update_bounds hr hh hhc with
⟨_, hpos, hbound, _, _, hcontract⟩
unfold nextPrecision stepVariance heat
rw [if_neg (not_le_of_gt hk)]
exact ⟨hpos, hbound, hcontract⟩
have finite_depth {κ c r₀ : ℝ} {η : ℕ → ℝ}
(hκ : 1 ≤ κ) (hc : 0 < c) (hc_upper : c < 1 / 4) (hr₀ : 0 ≤ r₀)
(hη : ∀ n, 0 < η n ∧ η n ≤ c) (M N : ℕ)
(hM : (4 / 5 : ℝ) ^ M * condition κ r₀ < 2) :
0 < (precision κ c r₀ η (M + 1 + N))⁻¹ ∧
(precision κ c r₀ η (M + 1 + N))⁻¹ ≤
2 * c * (2 * c / (1 + 2 * c)) ^ N := by
have hm := enters_well_conditioned hκ hc hc_upper hr₀ hη M hM
have hn (n : ℕ) := precision_nonneg hκ hc hr₀ (fun j => (hη j).1) n
have hp (n : ℕ) := precision_succ_pos hκ hc hr₀ (fun j => (hη j).1) n
have hw (n : ℕ) (hmn : M ≤ n) :=
well_conditioned_persists hκ hc hr₀ (fun j => (hη j).1) hmn hm
have hstep (n : ℕ) (hmn : M ≤ n) :=
well_branch_variance (hn n) (hη n).1 (hη n).2 (hw n hmn)
have hrho : 0 ≤ 2 * c / (1 + 2 * c) := by positivity
have hbase : (precision κ c r₀ η (M + 1))⁻¹ ≤ 2 * c :=
(hstep M le_rfl).2.1
constructor
· apply inv_pos.mpr
simpa only [Nat.add_assoc, Nat.add_comm 1 N] using hp (M + N)
· induction N with
| zero => simpa using hbase
| succ N ih =>
have hs := (hstep (M + 1 + N) (by omega)).2.2
(by simpa only [Nat.add_assoc, Nat.add_comm 1 N] using hp (M + N))
change (precision κ c r₀ η ((M + 1 + N) + 1))⁻¹ ≤
(2 * c / (1 + 2 * c)) * (precision κ c r₀ η (M + 1 + N))⁻¹ at hs
calc
(precision κ c r₀ η (M + 1 + (N + 1)))⁻¹
≤ (2 * c / (1 + 2 * c)) * (precision κ c r₀ η (M + 1 + N))⁻¹ :=
by simpa only [Nat.add_assoc] using hs
_ ≤ (2 * c / (1 + 2 * c)) * (2 * c * (2 * c / (1 + 2 * c)) ^ N) :=
mul_le_mul_of_nonneg_left ih hrho
_ = 2 * c * (2 * c / (1 + 2 * c)) ^ (N + 1) := by rw [pow_succ]; ring
have exists_terminal {κ c r₀ B : ℝ} {η : ℕ → ℝ}
(hκ : 1 ≤ κ) (hc : 0 < c) (hc_upper : c < 1 / 4) (hr₀ : 0 ≤ r₀)
(hη : ∀ n, 0 < η n ∧ η n ≤ c) (hB : 0 < B) :
∃ J : ℕ, 0 < J ∧ 0 < (precision κ c r₀ η J)⁻¹ ∧
(precision κ c r₀ η J)⁻¹ ≤ B := by
have hK : 0 < condition κ r₀ := lt_of_lt_of_le zero_lt_one (condition_bounds hκ hr₀)
obtain ⟨M, hM⟩ := exists_pow_lt_of_lt_one (div_pos (by norm_num : (0 : ℝ) < 2) hK)
(by norm_num : (4 / 5 : ℝ) < 1)
have hM' : (4 / 5 : ℝ) ^ M * condition κ r₀ < 2 := (lt_div_iff₀ hK).mp hM
have htwo : 0 < 2 * c := by positivity
have hrho : 2 * c / (1 + 2 * c) < 1 :=
(div_lt_one (by positivity)).2 (by linarith)
obtain ⟨N, hN⟩ := exists_pow_lt_of_lt_one (div_pos hB htwo) hrho
have hN' : 2 * c * (2 * c / (1 + 2 * c)) ^ N < B := by
simpa only [mul_comm] using (lt_div_iff₀ htwo).mp hN
have hf := finite_depth hκ hc hc_upper hr₀ hη M N hM'
exact ⟨M + 1 + N, by omega, hf.1, hf.2.trans hN'.le⟩
exact ⟨fun n => ⟨precision_nonneg hκ hc hr₀ (fun j => (hη j).1) n,
precision_succ_pos hκ hc hr₀ (fun j => (hη j).1) n⟩,
condition_sequence_antitone hκ hc hr₀ (fun j => (hη j).1),
fun m n hmn hm => well_conditioned_persists hκ hc hr₀
(fun j => (hη j).1) hmn hm,
fun M N hM => finite_depth hκ hc hc_upper hr₀ hη M N hM,
fun B hB => exists_terminal hκ hc hc_upper hr₀ hη hB⟩
end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.RecursiveDepthScope and omitted-condition boundaries
- Only deterministic parameter evolution defined by the source schedule. No stochastic kernel or adaptive-history measurability, FORS correctness/work, recursive distributional errors, actual-input expected query cost, or complete paper. The geometric depth certificate and existence of a finite threshold-hitting stage do not establish the specified logarithmic J and universal constants in equation(6.4).
Source and reuse
ASTIS parents called
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.RecursiveCondition.contraction_boundsAutoSamplingTheory.ExampleCases.SmoothedPicardHMC.RecursiveVariance.variance_update_bounds
Mathlib API called (external library)
- div_le_div_iff₀
- antitone_nat_of_succ_le
- le_geom
- exists_pow_lt_of_lt_one
Mathematical sources
- Chen, Chewi, Lu and Zhang, SPHMC v1, §6.2.2–6.3 — Source parameter schedule and geometric progress; expanded ASTIS proof, not a verbatim paper proof.
ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.