Actual RGO stopping depth and stability beyond the finite cap
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.StoppedRGODepth.stopped_rgo_depth · theorem · Teaching coverage
Mathematical statement
Let E be a finite-dimensional real inner-product Borel space of dimension d=finrank_R(E)>0 and mu a probability measure. Use states s=(b,u,k,h) in NNReal times E times Nat times E^Nat. Fix kappa≥1, 0<c<1/4, q≥2, 0<Delta≤1/2, 0<gamma≤1 and C≥8. Let eta be measurable on the full state and satisfy 0<eta(s)≤c everywhere. Fix initial s0 and arbitrary Markov observation and terminal kernels Q,Lterm. Define K(r)=(1+r)/(1/kappa+r), tau(r)=K(r) when K(r)≥2 and c otherwise, and a(s)=(eta(s)+tau(b))/(1+b). Compute ell=q+log(K(b0)*d*q/Delta), B=gamma/(sqrt(d*ell)+ell) and J=ceil(C*log(e*K(b0)/B)) once from s0. There exist an update F, a Markov state kernel P and Markov output kernels R_n. F adds 1/a(s) to precision, updates the center to (b*u+y/a(s))/(b+1/a(s)), increments the count and prepends y to history. P(s)=dirac s when 1/B≤b and is the F(s,.) pushforward of Q(s) otherwise. For all n, R_n=Lterm composed with P^n. B is positive, P^J(s0) assigns mass one to the terminal set {s:1/B≤b(s)}, and for every m, R_(J+m)(s0)=R_J(s0). Finally J≤(3*C+(C/2)*log(1/gamma))*ell.
Lean statement · stopped_rgo_depth
Actual source-shaped absorbed state program reaches its fixed initial-state terminal threshold at the explicit logarithmic depth and has stable output for every larger finite cap.
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 stopped_rgo_depth (μ : Measure E) [IsProbabilityMeasure μ]
(η : PS → ℝ) (hηm : Measurable η) (κ c q Δ γ C : ℝ)
(hκ : 1 ≤ κ) (hc : 0 < c) (hc1 : c < 1/4)
(hη : ∀ s, 0 < η s ∧ η s ≤ c) (hd : 0 < Module.finrank ℝ E) (hq : 2 ≤ q)
(hΔ : 0 < Δ) (hΔ1 : Δ ≤ 1/2) (hγ : 0 < γ) (hγ1 : γ ≤ 1) (hC : 8 ≤ C)
(s0 : PS) (Q Lterm : Kernel PS E) [IsMarkovKernel Q] [IsMarkovKernel Lterm] :
let K := fun r : ℝ => (1+r)/(κ⁻¹+r)
let τ := fun r : ℝ => if 2 ≤ K r then K r else c
let a := fun s : PS => (η s+τ s.1)/(1+s.1)
let L := q+Real.log (K s0.1*Module.finrank ℝ E*q/Δ)
let B := γ/(Real.sqrt (Module.finrank ℝ E*L)+L)
let J := Nat.ceil (C*Real.log (Real.exp 1*K s0.1/B))
∃ (F : PS × E → PS) (P : Kernel PS PS) (R : ℕ → Kernel PS E),
(∀ s y, ((F (s,y)).1 : ℝ) = (s.1 : ℝ)+(a s)⁻¹ ∧
(F (s,y)).2 =
(((s.1 : ℝ)+(a s)⁻¹)⁻¹ • ((s.1 : ℝ) • s.2.1+(a s)⁻¹ • y),
s.2.2.1+1,fun n => Nat.casesOn n y s.2.2.2)) ∧
IsMarkovKernel P ∧ (∀ n, IsMarkovKernel (R n)) ∧
(∀ s, P s = if B⁻¹ ≤ (s.1 : ℝ) then Measure.dirac s else
(Q s).map (fun y => F (s,y))) ∧
(∀ n, R n = Lterm ∘ₖ (P^n)) ∧
0 < B ∧ (P^J) s0 {s | B⁻¹ ≤ (s.1 : ℝ)} = 1 ∧
(∀ m, R (J+m) s0 = R J s0) ∧
(J : ℝ) ≤ (3*C+(C/2)*Real.log (1/γ))*LProof roadmap
- 1Construct the positive measurable source variance
K composed with the precision coordinate is measurable, as is its comparison with two. The piecewise heat duration is measurable and positive: on its first branch it is at least two, and on the other it is c>0. The positive eta and denominator 1+b give a positive measurable a. A call to LogarithmicDepth with the auxiliary constant sequence c extracts B>0 and the explicit J bound, which depend only on the initial parameters. This auxiliary call is not used to replace the actual history-dependent schedule.
- 2Instantiate the same explicit absorbed finite program
Invoke FiniteRGOProgram with a and the fixed nonnegative threshold 1/B. Its actual update F changes precision, center, count and history. It supplies P and all R_n with the stopped and continuing recursion. Define G(s,y)=s at terminal states and F(s,y) elsewhere. P(s) is also the G(s,.) pushforward of Q(s): on the stopped branch a probability measure pushed through a constant map is dirac s. This representation does not add actual calls after stopping.
- 3Prove every observation path reaches the threshold
For an arbitrary observation sequence, follow the actual absorbed state path x_n. Define eta_n=eta(x_n), which satisfies the same positive upper bound on every path. Compare its precision with the unabsorbed scalar recursion driven by this particular sequence. Induction proves that x_n has already stopped or its precision equals that recursion. Apply LogarithmicDepth to eta_n. At J the auxiliary inverse precision is at most B, so either branch of the invariant implies that x_J is terminal. This is a pathwise use of a universally quantified sequence theorem, not a common schedule assumption.
- 4Transfer the pathwise conclusion to the actual law
For any depth n, if every observation sequence from a state has endpoint in a measurable set D, prove that P^n assigns D mass one. The zero-depth case is a point mass. For the successor, express P as the pushforward under G and integrate the n-step event mass. Each possible first observation leaves a shorter path whose every continuation ends in D, so the induction hypothesis makes the integrand one. Apply this result to the pathwise J bound and the measurable terminal set.
- 5Identify recursive outputs with transition powers
Use the actual finite-program recursion to show R_(n+1)=R_n composed with P. At stopped states, the point-mass transition and the already proved stopped output R_n(s)=Lterm(s) give the equality. On continuing states, pushforward integration gives precisely the same recursive bind. Induction starting from R_0=Lterm yields R_n=Lterm composed with P^n.
- 6Remove every larger finite cap at the fixed initial state
Split J+m transitions into the first J and the remaining m. The J-step law is concentrated on terminal states, and on those states R_m equals Lterm. Their equality holds almost everywhere under that actual law, so binding with R_m or Lterm gives the same measure. This proves R_(J+m)(s0)=R_J(s0) for every m. It eliminates premature cap use for this execution without identifying the terminal sampler or its query cost.
Full assumptions and notation
All objects and hypotheses
- E is finite-dimensional over the reals with its Borel measurable structure, and d=finrank_R(E)>0. mu is any probability measure; no density or moment assumption is added.
- kappa≥1, 0<c<1/4, q≥2, 0<Delta≤1/2, 0<gamma≤1 and C≥8 are explicit scalar conditions.
- eta is measurable and lies in (0,c] at every state. It may depend on precision, center, count and full padded history; there is no common predetermined sequence across all paths.
- s0 is fixed before the terminal variance B, its inverse precision threshold and J are computed. These remain fixed throughout the entire execution.
- Q and Lterm are arbitrary Markov kernels. The actual absorbed update and all finite output kernels are constructed using FiniteRGOProgram.
- Source formulas correspond to baseline smoothness one. Initial precision may be zero or already beyond the threshold. Arbitrary starting count/history is not asserted to be a valid record of previous calls.
Mathematical proof
1. Construct the positive measurable source variance
K composed with the precision coordinate is measurable, as is its comparison with two. The piecewise heat duration is measurable and positive: on its first branch it is at least two, and on the other it is c>0. The positive eta and denominator 1+b give a positive measurable a. A call to LogarithmicDepth with the auxiliary constant sequence c extracts B>0 and the explicit J bound, which depend only on the initial parameters. This auxiliary call is not used to replace the actual history-dependent schedule.
Corresponding Lean step
Local source_variance; Measurable.ite; first LogarithmicDepth.terminal_depth invocation with constant c only for threshold positivity and the initial-data depth bound.
2. Instantiate the same explicit absorbed finite program
Invoke FiniteRGOProgram with a and the fixed nonnegative threshold 1/B. Its actual update F changes precision, center, count and history. It supplies P and all R_n with the stopped and continuing recursion. Define G(s,y)=s at terminal states and F(s,y) elsewhere. P(s) is also the G(s,.) pushforward of Q(s): on the stopped branch a probability measure pushed through a constant map is dirac s. This representation does not add actual calls after stopping.
Corresponding Lean step
FiniteRGOProgram.finite_rgo_program; measurable product update, Measurable.ite, hPmap and Measure.map_const.
3. Prove every observation path reaches the threshold
For an arbitrary observation sequence, follow the actual absorbed state path x_n. Define eta_n=eta(x_n), which satisfies the same positive upper bound on every path. Compare its precision with the unabsorbed scalar recursion driven by this particular sequence. Induction proves that x_n has already stopped or its precision equals that recursion. Apply LogarithmicDepth to eta_n. At J the auxiliary inverse precision is at most B, so either branch of the invariant implies that x_J is terminal. This is a pathwise use of a universally quantified sequence theorem, not a common schedule assumption.
Corresponding Lean step
Local absorbed_precision_path and pathwise_log_depth; second LogarithmicDepth.terminal_depth invocation uses the actual path eta(x_n).
4. Transfer the pathwise conclusion to the actual law
For any depth n, if every observation sequence from a state has endpoint in a measurable set D, prove that P^n assigns D mass one. The zero-depth case is a point mass. For the successor, express P as the pushforward under G and integrate the n-step event mass. Each possible first observation leaves a shorter path whose every continuation ends in D, so the induction hypothesis makes the integrand one. Apply this result to the pathwise J bound and the measurable terminal set.
Corresponding Lean step
Local statePath_shift and path_endpoint_mass; Kernel.comp_apply, lintegral_map and probability normalization.
5. Identify recursive outputs with transition powers
Use the actual finite-program recursion to show R_(n+1)=R_n composed with P. At stopped states, the point-mass transition and the already proved stopped output R_n(s)=Lterm(s) give the equality. On continuing states, pushforward integration gives precisely the same recursive bind. Induction starting from R_0=Lterm yields R_n=Lterm composed with P^n.
Corresponding Lean step
Main hRstep and hRp; actual hrec/hstop from FiniteRGOProgram, Measure.dirac_bind, Measure.bind_apply, lintegral_map and Kernel.comp_assoc.
6. Remove every larger finite cap at the fixed initial state
Split J+m transitions into the first J and the remaining m. The J-step law is concentrated on terminal states, and on those states R_m equals Lterm. Their equality holds almost everywhere under that actual law, so binding with R_m or Lterm gives the same measure. This proves R_(J+m)(s0)=R_J(s0) for every m. It eliminates premature cap use for this execution without identifying the terminal sampler or its query cost.
Corresponding Lean step
Local finite_output_stability; mem_ae_iff_prob_eq_one, Measure.bind_congr_right, pow_add and Kernel.comp_assoc.
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · stopped_rgo_depth
Measurable positive source variance, actual finite-program construction, pathwise depth, kernel-support induction and terminal almost-everywhere output identity.
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 stopped_rgo_depth (μ : Measure E) [IsProbabilityMeasure μ]
(η : PS → ℝ) (hηm : Measurable η) (κ c q Δ γ C : ℝ)
(hκ : 1 ≤ κ) (hc : 0 < c) (hc1 : c < 1/4)
(hη : ∀ s, 0 < η s ∧ η s ≤ c) (hd : 0 < Module.finrank ℝ E) (hq : 2 ≤ q)
(hΔ : 0 < Δ) (hΔ1 : Δ ≤ 1/2) (hγ : 0 < γ) (hγ1 : γ ≤ 1) (hC : 8 ≤ C)
(s0 : PS) (Q Lterm : Kernel PS E) [IsMarkovKernel Q] [IsMarkovKernel Lterm] :
let K := fun r : ℝ => (1+r)/(κ⁻¹+r)
let τ := fun r : ℝ => if 2 ≤ K r then K r else c
let a := fun s : PS => (η s+τ s.1)/(1+s.1)
let L := q+Real.log (K s0.1*Module.finrank ℝ E*q/Δ)
let B := γ/(Real.sqrt (Module.finrank ℝ E*L)+L)
let J := Nat.ceil (C*Real.log (Real.exp 1*K s0.1/B))
∃ (F : PS × E → PS) (P : Kernel PS PS) (R : ℕ → Kernel PS E),
(∀ s y, ((F (s,y)).1 : ℝ) = (s.1 : ℝ)+(a s)⁻¹ ∧
(F (s,y)).2 =
(((s.1 : ℝ)+(a s)⁻¹)⁻¹ • ((s.1 : ℝ) • s.2.1+(a s)⁻¹ • y),
s.2.2.1+1,fun n => Nat.casesOn n y s.2.2.2)) ∧
IsMarkovKernel P ∧ (∀ n, IsMarkovKernel (R n)) ∧
(∀ s, P s = if B⁻¹ ≤ (s.1 : ℝ) then Measure.dirac s else
(Q s).map (fun y => F (s,y))) ∧
(∀ n, R n = Lterm ∘ₖ (P^n)) ∧
0 < B ∧ (P^J) s0 {s | B⁻¹ ≤ (s.1 : ℝ)} = 1 ∧
(∀ m, R (J+m) s0 = R J s0) ∧
(J : ℝ) ≤ (3*C+(C/2)*Real.log (1/γ))*L := by
classical
let statePath (G : PS × E → PS) (s : PS) (ys : ℕ → E) : ℕ → PS :=
Nat.rec s (fun n x => G (x,ys n))
have statePath_shift (G : (PS) × E → (PS)) (n : ℕ) (s : (PS)) (ys : ℕ → E) :
statePath G s ys (n+1) = statePath G (G (s,ys 0)) (fun k => ys (k+1)) n := by
induction n with
| zero => rfl
| succ n ih =>
change G (statePath G s ys (n+1),ys (n+1)) =
G (statePath G (G (s,ys 0)) (fun k => ys (k+1)) n,ys (n+1))
rw [ih]
have path_endpoint_mass (G : (PS) × E → (PS)) (hG : Measurable G)
(Q : Kernel (PS) E) [IsMarkovKernel Q] (P : Kernel (PS) (PS)) [IsMarkovKernel P]
(hP : ∀ s, P s = (Q s).map (fun y => G (s,y)))
(D : Set (PS)) (hD : MeasurableSet D) (n : ℕ) (s : (PS))
(hpaths : ∀ ys : ℕ → E, statePath G s ys n ∈ D) [Nonempty E] :
(P^n) s D = 1 := by
have hp (k : ℕ) : IsMarkovKernel (P^k) := by
induction k with
| zero => change IsMarkovKernel Kernel.id; infer_instance
| succ k ih =>
let := ih
rw [pow_succ]
change IsMarkovKernel ((P^k) ∘ₖ P)
infer_instance
induction n generalizing s with
| zero =>
classical
have hs := hpaths (fun _ => Classical.choice inferInstance)
change Measure.dirac s D = 1
exact Measure.dirac_apply_of_mem hs
| succ n ih =>
let := hp n
rw [pow_succ]
change ((P^n) ∘ₖ P) s D = 1
rw [Kernel.comp_apply' _ _ _ hD,hP,
lintegral_map ((P^n).measurable_coe hD)
(show Measurable (fun y : E => G (s,y)) from hG.comp measurable_prodMk_left)]
have hall (y : E) : (P^n) (G (s,y)) D = 1 := by
apply ih
intro ys
have hh := hpaths (fun k => Nat.casesOn k y ys)
rw [statePath_shift] at hh
exact hh
simp_rw [hall]
simp
have absorbed_precision_path (b : (PS) → ℝ) (η : (PS) → ℝ) (τ : ℝ → ℝ)
(F : (PS) × E → (PS)) (threshold : ℝ)
(hF : ∀ s y, b (F (s,y)) = b s + ((η s + τ (b s))/(1+b s))⁻¹)
(s0 : (PS)) (ys : ℕ → E) :
let G : (PS) × E → (PS) := fun p => if threshold ≤ b p.1 then p.1 else F p
let x := statePath G s0 ys
let r : ℕ → ℝ := Nat.rec (b s0) (fun n r => r + ((η (x n)+τ r)/(1+r))⁻¹)
∀ n, threshold ≤ b (x n) ∨ b (x n) = r n := by
classical
intro G x r n
induction n with
| zero => exact Or.inr rfl
| succ n ih =>
have hx : x (n+1) = G (x n,ys n) := rfl
by_cases hs : threshold ≤ b (x n)
· left
rw [hx,show G (x n,ys n) = x n from if_pos hs]
exact hs
· right
have heq := ih.resolve_left hs
rw [hx,show G (x n,ys n) = F (x n,ys n) from if_neg hs,hF]
change b (x n) + ((η (x n)+τ (b (x n)))/(1+b (x n)))⁻¹ =
r n + ((η (x n)+τ (r n))/(1+r n))⁻¹
rw [heq]
have pathwise_log_depth (b : (PS) → ℝ) (η : (PS) → ℝ) (F : (PS) × E → (PS))
(κ c q Δ γ C : ℝ) (d : ℕ) (s0 : (PS))
(hκ : 1 ≤ κ) (hc : 0 < c) (hc1 : c < 1/4) (hb0 : 0 ≤ b s0)
(hη : ∀ s, 0 < η s ∧ η s ≤ c) (hd : 0 < d) (hq : 2 ≤ q)
(hΔ : 0 < Δ) (hΔ1 : Δ ≤ 1/2) (hγ : 0 < γ) (hγ1 : γ ≤ 1) (hC : 8 ≤ C) :
let K := fun r : ℝ => (1+r)/(κ⁻¹+r)
let τ := fun r : ℝ => if 2 ≤ K r then K r else c
let L := q+Real.log (K (b s0)*d*q/Δ)
let B := γ/(Real.sqrt (d*L)+L)
let J := Nat.ceil (C*Real.log (Real.exp 1*K (b s0)/B))
(∀ s y, b (F (s,y)) = b s + ((η s+τ (b s))/(1+b s))⁻¹) →
∀ ys : ℕ → E,
let G : (PS) × E → (PS) := fun p => if B⁻¹ ≤ b p.1 then p.1 else F p
B⁻¹ ≤ b (statePath G s0 ys J) := by
classical
intro K τ L B J hF ys G
let x := statePath G s0 ys
let r : ℕ → ℝ := Nat.rec (b s0) (fun n r => r + ((η (x n)+τ r)/(1+r))⁻¹)
have hh := AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.LogarithmicDepth.terminal_depth
(η := fun n => η (x n)) hκ hc hc1 hb0 (fun n => hη (x n)) hd hq hΔ hΔ1 hγ hγ1 hC
change 2 ≤ L ∧ (0 < B ∧ B ≤ 1) ∧ 0 < J ∧ 0 < (r J)⁻¹ ∧ (r J)⁻¹ ≤ B ∧ _ at hh
obtain ⟨hL,hB,hJ,hrpos,hrB,hJbound⟩ := hh
have hr : 0 < r J := inv_pos.mp hrpos
have hbJ : B⁻¹ ≤ r J := by
rw [inv_eq_one_div]
apply (div_le_iff₀ hB.1).2
have hm : 1 ≤ B * r J := (div_le_iff₀ hr).1 (by simpa [one_div] using hrB)
simpa [mul_comm] using hm
have hinv := absorbed_precision_path b η τ F B⁻¹ hF s0 ys J
change B⁻¹ ≤ b (x J) ∨ b (x J) = r J at hinv
rcases hinv with h | h
· exact h
· change B⁻¹ ≤ b (x J)
rw [h]
exact hbJ
have source_variance (b : (PS) → ℝ) (hb : Measurable b) (hb0 : ∀ s, 0 ≤ b s)
(η : (PS) → ℝ) (hη : Measurable η) (hη0 : ∀ s, 0 < η s) (κ c : ℝ) (hc : 0 < c) :
let K := fun s => (1+b s)/(κ⁻¹+b s)
let τ := fun s => if 2 ≤ K s then K s else c
let a := fun s => (η s+τ s)/(1+b s)
Measurable a ∧ ∀ s, 0 < a s := by
intro K τ a
have hK : Measurable K := by dsimp [K]; fun_prop
have hτ : Measurable τ := Measurable.ite
(measurableSet_le measurable_const hK) hK measurable_const
refine ⟨(hη.add hτ).div (measurable_const.add hb),?_⟩
intro s
have ht : 0 < τ s := by
dsimp only [τ]
split_ifs with h
· linarith
· exact hc
exact div_pos (add_pos (hη0 s) ht) (by linarith [hb0 s])
have finite_output_stability (P : Kernel (PS) (PS)) [IsMarkovKernel P]
(L : Kernel (PS) E) [IsMarkovKernel L] (R : ℕ → Kernel (PS) E)
(hR : ∀ n, R n = L ∘ₖ (P^n)) (D : Set (PS)) (hD : MeasurableSet D)
(hstop : ∀ n s, s ∈ D → R n s = L s) (J : ℕ) (s : (PS))
(hmass : (P^J) s D = 1) : ∀ m, R (J+m) s = R J s := by
have hp (k : ℕ) : IsMarkovKernel (P^k) := by
induction k with
| zero => change IsMarkovKernel Kernel.id; infer_instance
| succ k ih =>
let := ih
rw [pow_succ]
change IsMarkovKernel ((P^k) ∘ₖ P)
infer_instance
let := hp J
have hae : ∀ᵐ t ∂((P^J) s), t ∈ D := (mem_ae_iff_prob_eq_one hD).2 hmass
intro m
let := hp m
rw [hR (J+m),Nat.add_comm J m,pow_add]
change (L ∘ₖ ((P^m) ∘ₖ (P^J))) s = R J s
rw [← Kernel.comp_assoc,← hR m,hR J,Kernel.comp_apply,Kernel.comp_apply]
apply Measure.bind_congr_right
filter_upwards [hae] with t ht
exact hstop m t ht
intro K τ a L B J
have hb : Measurable (fun s : PS => (s.1 : ℝ)) := by fun_prop
have hva := source_variance (fun s : PS => (s.1 : ℝ)) hb (fun s => s.1.coe_nonneg)
η hηm (fun s => (hη s).1) κ c hc
change Measurable a ∧ (∀ s, 0 < a s) at hva
obtain ⟨ha,ha0⟩ := hva
have hdepth := AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.LogarithmicDepth.terminal_depth
(r₀ := (s0.1 : ℝ)) (η := fun _ => c) hκ hc hc1 s0.1.coe_nonneg
(fun _ => ⟨hc,le_rfl⟩) hd hq hΔ hΔ1 hγ hγ1 hC
change 2 ≤ L ∧ (0 < B ∧ B ≤ 1) ∧ 0 < J ∧ _ ∧ _ ∧
(J : ℝ) ≤ (3*C+(C/2)*Real.log (1/γ))*L at hdepth
have hB := hdepth.2.1.1
have hJB := hdepth.2.2.2.2.2
let threshold : ℝ≥0 := ⟨B⁻¹,le_of_lt (inv_pos.mpr hB)⟩
let F : PS × E → PS := fun p =>
(⟨(p.1.1 : ℝ)+(a p.1)⁻¹, add_nonneg p.1.1.coe_nonneg (le_of_lt (inv_pos.mpr (ha0 p.1)))⟩,
((p.1.1 : ℝ)+(a p.1)⁻¹)⁻¹ • ((p.1.1 : ℝ) • p.1.2.1+(a p.1)⁻¹ • p.2),
p.1.2.2.1+1, fun n => Nat.casesOn n p.2 p.1.2.2.2)
have hF : Measurable F := by
apply Measurable.prodMk
· exact Measurable.subtype_mk (by fun_prop)
· apply Measurable.prodMk
· fun_prop
· apply Measurable.prodMk
· fun_prop
· apply measurable_pi_lambda
intro n
cases n <;> fun_prop
obtain ⟨T,H,hT,hH,hTf,hHf,hprog⟩ :=
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.FiniteRGOProgram.finite_rgo_program μ a ha ha0 threshold
obtain ⟨P,R,hP,hR,hPf,hzero,hrec,hstop,hpath,hideal⟩ := hprog Q Lterm inferInstance inferInstance
let := hP
let D : Set PS := {s | B⁻¹ ≤ (s.1 : ℝ)}
have hD : MeasurableSet D := measurableSet_le measurable_const hb
let G : PS × E → PS := fun p => if B⁻¹ ≤ (p.1.1 : ℝ) then p.1 else F p
have hG : Measurable G := Measurable.ite
(measurableSet_le measurable_const (hb.comp measurable_fst)) measurable_fst hF
have hcompare (s : PS) : (threshold ≤ s.1) ↔ B⁻¹ ≤ (s.1 : ℝ) := Iff.rfl
have hPf' (s : PS) : P s = if B⁻¹ ≤ (s.1 : ℝ) then Measure.dirac s else
(Q s).map (fun y => F (s,y)) := by
rw [hPf]
rfl
have hPmap (s : PS) : P s = (Q s).map (fun y => G (s,y)) := by
rw [hPf']
by_cases hs : B⁻¹ ≤ (s.1 : ℝ)
· simp only [if_pos hs,G]
simp [Measure.map_const]
· simp only [if_neg hs,G]
have hmass : (P^J) s0 D = 1 := by
apply path_endpoint_mass G hG Q P hPmap D hD J s0
intro ys
exact pathwise_log_depth (fun s : PS => (s.1 : ℝ)) η F κ c q Δ γ C
(Module.finrank ℝ E) s0 hκ hc hc1 s0.1.coe_nonneg hη hd hq hΔ hΔ1 hγ hγ1 hC
(fun _ _ => rfl) ys
have hRstep (n : ℕ) : R (n+1) = R n ∘ₖ P := by
ext s t ht
rw [Kernel.comp_apply,hPf,hrec]
by_cases hs : threshold ≤ s.1
· rw [if_pos hs,if_pos hs,Measure.dirac_bind (R n).measurable,hstop n s hs]
· rw [if_neg hs,if_neg hs]
change ((Q s).bind (fun y => R n (F (s,y)))) t =
(((Q s).map (fun y => F (s,y))).bind (R n)) t
rw [Measure.bind_apply ht (show AEMeasurable (fun y : E => R n (F (s,y))) (Q s)
from ((R n).measurable.comp (hF.comp measurable_prodMk_left)).aemeasurable),
Measure.bind_apply ht (R n).aemeasurable]
exact (lintegral_map ((R n).measurable_coe ht)
(show Measurable (fun y : E => F (s,y)) from hF.comp measurable_prodMk_left)).symm
have hRp (n : ℕ) : R n = Lterm ∘ₖ (P^n) := by
induction n with
| zero =>
change R 0 = Lterm ∘ₖ Kernel.id
rw [Kernel.comp_id,hzero]
| succ n ih =>
rw [hRstep,ih,pow_succ]
exact Kernel.comp_assoc Lterm (P^n) P
refine ⟨F,P,R,fun _ _ => ⟨rfl,rfl⟩,hP,hR,hPf',hRp,hB,hmass,?_,hJB⟩
exact finite_output_stability P Lterm R hRp D hD
(fun n s hs => hstop n s ((hcompare s).2 hs)) J s0 hmass
end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.StoppedRGODepthSource assumptions versus formal assumptions
| Source | Actual Lean | Difference kind | Why it matters |
|---|---|---|---|
| The paper uses a Euclidean Gibbs target. | Any probability base on a positive-dimensional finite real Hilbert Borel space. | generalization | The actual state transition bound does not need a potential, density or moments. d is the real finrank and strictly positive. |
| Normalized recursive variance is (eta+tau)/beta_A, with condition number determined by the current regularization. | a(s)=(eta(s)+tau(b))/(1+b), K(b)=(1+b)/(kappa^-1+b). | API-limitation | These are the source scalar formulas after baseline smoothness is normalized to one. A general beta needs its scaling adapter; arbitrary Q is not identified as the concrete sampler. |
| A terminal level is fixed for the recursive execution; equation(6.4) selects a logarithmic stage bound. | Compute B and J from s0 once, then construct the fixed-threshold P and all R. | same | The result is at that initial state. It does not claim all initial states share a threshold or one uniform J. |
| Sufficiently small and large universal constants select the terminal level and depth. | 0<c<1/4,0<gamma<=1,C>=8; J<=(3C+(C/2)log(1/gamma))*ell. | source-implicit | The sufficient depth constant and threshold-dependent coefficient come from the already proved LogarithmicDepth; C>=8 is not quoted as a source-prescribed value. |
| The smoothing level is selected for each call and bounded by c. | Measurable eta on the full current state with 0<eta(s)<=c; actual absorbed paths induce their own eta sequences. | source-implicit | There is no common fixed schedule. The constant sequence call only extracts initial-parameter threshold positivity and J bound; termination uses actual path eta. |
| Full recursive sampler has FORS, approximation guarantees and query costs. | Any Markov Q,Lterm yield terminal support mass one by J and unchanged output at every larger cap. | API-limitation | This is an actual stage-transition bound and cap-removal prerequisite. It does not identify either concrete sampler, prove history validity or bound errors/gradient queries. |
The terminal threshold and stage bound are computed from the initial state and then fixed. The scalar source formulas use smoothness normalized to one; a general smoothness parameter needs the source scaling adapter. The actual dimension is positive. C>=8 is a proved sufficient constant, not a source-prescribed numerical value. Arbitrary observation and terminal Markov kernels do not identify the concrete smoothed sampler or FORS. Stage transitions are not gradient queries. No initialization validity, approximation error or expected query-cost result is asserted, and no uniform kernel equality across all initial states is claimed.
Encoder–denoiser: accepted · domain-mismatch
Detected semantic differences
- domains: General probability/Hilbert setting with actual positive finrank. — No density, curvature or moments. mu supports parent-program reuse and does not constrain the supplied Q,Lterm in the conclusion.
- constant_dependencies: Normalized smoothness-one variance formulas; general scaling adapter remains. — Baseline smoothness one disclosed. C>=8 is a proved sufficient choice; upper coefficient retains (C/2)log(1/gamma).
- quantifiers: Threshold and J are computed from s0 once and fixed. — Every P fiber uses the fixed B; no whole-kernel output equality at a globally uniform J.
- constant_dependencies: Explicit sufficient depth constants and gamma coefficient are not full FORS constant guarantees. — Baseline smoothness one disclosed. C>=8 is a proved sufficient choice; upper coefficient retains (C/2)log(1/gamma).
- assumptions: Pathwise eta(x_n) varies with history; constant-c invocation only establishes initial-data B positivity/J bound. — No stopping, favorable support, accuracy or common schedule is assumed. The gamma range is for depth only, not asserted sufficient for FORS.
- scopes: Arbitrary supplied kernels receive stage-depth and cap-stability, without concrete sampler, errors or costs. — Concrete sampler, history validity, errors and query counts remain excluded. Stage transitions are not gradient queries.
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
- The terminal threshold and stage bound are computed from the initial state and then fixed. The scalar source formulas use smoothness normalized to one; a general smoothness parameter needs the source scaling adapter. The actual dimension is positive. C≥8 is a proved sufficient constant, not a source-prescribed numerical value. Arbitrary observation and terminal Markov kernels do not identify the concrete smoothed sampler or FORS. Stage transitions are not gradient queries. No initialization validity, approximation error or expected query-cost result is asserted, and no uniform kernel equality across all initial states is claimed.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.FiniteRGOProgram.finite_rgo_programAutoSamplingTheory.ExampleCases.SmoothedPicardHMC.LogarithmicDepth.terminal_depth
Mathlib API called (external library)
- Measurable.ite
- MeasureTheory.Measure.map_const
- ProbabilityTheory.Kernel.comp_assoc
- MeasureTheory.Measure.bind_apply
- MeasureTheory.lintegral_map
- MeasureTheory.mem_ae_iff_prob_eq_one
- MeasureTheory.Measure.bind_congr_right
Mathematical sources
- SPHMC v1 Algorithm 3.3 and Theorem 6.5, equations (6.2)-(6.4) — Actual absorbed state execution with source-shaped variance and fixed initial-state terminal level; not error or gradient-query complexity.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.