Actual stopped Gaussian RGO output correctness under sampler interfaces
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.StoppedGaussianRGOError.stopped_gaussian_rgo_error · theorem · Teaching coverage
Statement
Let E be a finite-dimensional real inner-product Borel space of positive real dimension d, and mu a probability measure. States s=(b,u,k,h) belong to NNReal times E times Nat times E^Nat. Let eta be measurable with 0<eta(s)<=c at every state. Assume kappa>=1, 0<c<1/4, 0<Delta<=1/2, 0<gamma<=1 and C>=8. Fix s0. Define K(r)=(1+r)/(1/kappa+r), tau(r)=K(r) if K(r)>=2 and c otherwise, a(s)=(eta(s)+tau(b))/(1+b), ell=2+log(K(b0)*d*2/Delta), B=gamma/(sqrt(d*ell)+ell), J=ceil(C*log(e*K(b0)/B)), and D={s:1/B<=b}. There exist Markov T,H with T(s) the normalized quadratic tilt of mu at precision b and center u, and H(s) its Gaussian smoothing at standard deviation sqrt(a(s)). After T,H are fixed, take any Markov M,L such that at each s outside D, squared W2(M(s),GaussianSmoothing(T(s),sqrt(eta(s)/(1+b))))<=ofReal(K(b)*[2*tau(b)*Delta^2/(K(b)*(J+1))]/(1+b)). There exist F,Q,P,R: F updates precision to b+1/a(s), center to (b*u+y/a(s))/(b+1/a(s)), count to k+1 and prepends y to history; Q(s) is M(s) with independent Gaussian variance tau(b)/(1+b) added; P(s)=dirac s on D and otherwise the F(s,.) pushforward of Q(s). Q,P and all R_n are Markov and R_n=L composed with P^n. B>0, P^J(s0)(D)=1, and R_(J+m)(s0)=R_J(s0) for all m. Without terminal accuracy assumptions, KL(R_J(s0)||T(s0))<=J*ofReal(Delta^2/(J+1))+integral over D of KL(L(x)||T(x)) under P^J(s0). If KL(L(s)||T(s))<=ofReal(Delta^2/(J+1)) holds for every s in D, then KL(R_(J+m)(s0)||T(s0))<=ofReal(Delta^2) for every natural m.
All objects and hypotheses
- E has its Borel structure and actual dimension d=finrank_R(E)>0; mu is any probability measure.
- kappa>=1,0<c<1/4,0<Delta<=1/2,0<gamma<=1,C>=8; eta is measurable and in (0,c] at every state.
- q=2 is fixed. B and J are computed once from the fixed initial state s0 and used throughout execution.
- M,L are Markov kernels. Only states outside D require the displayed source-scaled squared-W2 premise for M.
- Terminal KL is unrestricted for the residual inequality. Only the final total-error implication assumes its bound on D; no condition is imposed outside D.
Mathematical proof
1. Fix source parameters and the terminal threshold
Compose the precision coordinate with the rational conditioning function K; positivity follows from kappa>=1 and nonnegative precision. Its branch tau is measurable and positive. Apply LogarithmicDepth with the auxiliary constant sequence c and q=2 to obtain B>0, so 1/B defines a nonnegative threshold. This preliminary call does not establish termination of the actual path.
Corresponding Lean step
hKm,hKpos,htm,htpos; auxiliary LogarithmicDepth.terminal_depth and threshold theta.
2. Construct the actual source-accuracy program
Instantiate GaussianRGOErrorBudget with beta(s)=1+b and kappa(s)=K(b), not the baseline kappa. Its T,H precede the actual M,L. From the continuing-state W2 premise, obtain the actual added-noise Q and the explicit update F, absorbed transition P and recursive outputs R. Retain its finite-depth error bound and terminal residual.
Corresponding Lean step
GaussianRGOErrorBudget.gaussian_rgo_error_budget and hprog M L.
3. Prove that the stopping theorem uses the same transition
Call StoppedRGODepth with the actual Q and the same L and initial parameters. It returns another update and transition. Prove the two updates equal using the real precision coordinate and every remaining coordinate. Their transition fibers then agree because their Q and fixed threshold agree. This transfers the stopping theorem to the actual error program, rather than assuming existential witnesses coincide.
Corresponding Lean step
StoppedRGODepth.stopped_rgo_depth; hFeq via Prod.ext and Subtype.ext; hPeq via kernel extensionality and threshold coercion.
4. Align output kernels and transfer cap stability
Recover measurability of the actual F from its explicit coordinate formula. For the recursive outputs, prove R_(n+1)=R_n composed with P by splitting stopped and continuing states and using pushforward integration. Induction gives R_n=L composed with P^n. The stopping theorem gives the same formula for its outputs, hence the two output families agree, and stability beyond J transfers to the actual family.
Corresponding Lean step
hFexact,hFm; local recursive_output_powers; hRp,hReq and hstable'.
5. Restrict the residual to the actual terminal set
The transferred stopping theorem states that the actual law P^J(s0) gives D mass one. Convert this to almost-everywhere terminal membership, hence restriction to D leaves that measure unchanged. Apply the Gaussian budget at exactly J and rewrite its residual as the integral over D. This step needs no terminal KL bound and includes infinite residual.
Corresponding Lean step
hmass; mem_ae_iff_prob_eq_one, restrict_eq_self_of_ae_mem and hbound J s0.
6. Use terminal-only accuracy and then output stability
Assume the terminal KL interface only on D. The actual J-step law is almost surely in D, so nonnegative integral monotonicity bounds its residual by one allocation. Add the J observation allocations and use (J+1)*Delta^2/(J+1)=Delta^2. Finally transfer that J-depth bound to every J+m via the already proved equality of output laws. Applying the general linear budget at J+m would not establish this conclusion.
Corresponding Lean step
hterminal,lintegral_mono_ae,probability normalization,ENNReal.ofReal arithmetic and hstable'.
Lean statement · stopped_gaussian_rgo_error
Actual stopped Gaussian RGO output correctness under supplied A1 and terminal KL interfaces.
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_gaussian_rgo_error (μ : Measure E) [IsProbabilityMeasure μ]
(η : PS → ℝ) (hηm : Measurable η) (κ c Δ γ C : ℝ)
(hκ : 1 ≤ κ) (hc : 0 < c) (hc1 : c < 1/4)
(hη : ∀ s, 0 < η s ∧ η s ≤ c) (hd : 0 < Module.finrank ℝ E)
(hΔ : 0 < Δ) (hΔ1 : Δ ≤ 1/2) (hγ : 0 < γ) (hγ1 : γ ≤ 1) (hC : 8 ≤ C) (s0 : PS) :
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 ell := 2+Real.log (K s0.1*Module.finrank ℝ E*2/Δ)
let B := γ/(Real.sqrt (Module.finrank ℝ E*ell)+ell)
let J := Nat.ceil (C*Real.log (Real.exp 1*K s0.1/B))
let D : Set PS := {s | B⁻¹ ≤ (s.1:ℝ)}
∃ T H : Kernel PS E, IsMarkovKernel T ∧ IsMarkovKernel H ∧
(∀ s, T s = μ.tilted (fun x => -((s.1:ℝ)/2)*‖x-s.2.1‖^2)) ∧
(∀ s, H s = GaussianSmoothing.gaussianSmoothing (T s) (Real.sqrt (a s))) ∧
∀ M L : Kernel PS E, IsMarkovKernel M → IsMarkovKernel L →
(∀ s, s ∉ D → WassersteinSpace.wassersteinDistance (M s)
(GaussianSmoothing.gaussianSmoothing (T s) (Real.sqrt (η s/(1+s.1))))^2 ≤
ENNReal.ofReal (K s.1*(2*τ s.1*Δ^2/(K s.1*((J:ℝ)+1)))/(1+s.1))) →
∃ (F : PS × E → PS) (Q : Kernel PS E) (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 Q ∧ IsMarkovKernel P ∧ (∀ n, IsMarkovKernel (R n)) ∧
(∀ s, Q s = GaussianSmoothing.gaussianSmoothing (M s) (Real.sqrt (τ s.1/(1+s.1)))) ∧
(∀ s, P s = if s ∈ D then Measure.dirac s else (Q s).map (fun y => F (s,y))) ∧
(∀ n, R n = L ∘ₖ (P^n)) ∧
0 < B ∧ (P^J) s0 D = 1 ∧
(∀ m, R (J+m) s0 = R J s0) ∧
klDiv (R J s0) (T s0) ≤ (J:ℝ≥0∞)*ENNReal.ofReal (Δ^2/((J:ℝ)+1)) +
∫⁻ x in D, klDiv (L x) (T x) ∂(P^J) s0 ∧
((∀ s ∈ D, klDiv (L s) (T s) ≤ ENNReal.ofReal (Δ^2/((J:ℝ)+1))) →
∀ m, klDiv (R (J+m) s0) (T s0) ≤ ENNReal.ofReal (Δ^2))Lean proof · stopped_gaussian_rgo_error
Source schedule, actual Gaussian program, explicit witness equality, recursive powers, terminal support restriction and J-budget plus cap stability.
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_gaussian_rgo_error (μ : Measure E) [IsProbabilityMeasure μ]
(η : PS → ℝ) (hηm : Measurable η) (κ c Δ γ C : ℝ)
(hκ : 1 ≤ κ) (hc : 0 < c) (hc1 : c < 1/4)
(hη : ∀ s, 0 < η s ∧ η s ≤ c) (hd : 0 < Module.finrank ℝ E)
(hΔ : 0 < Δ) (hΔ1 : Δ ≤ 1/2) (hγ : 0 < γ) (hγ1 : γ ≤ 1) (hC : 8 ≤ C) (s0 : PS) :
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 ell := 2+Real.log (K s0.1*Module.finrank ℝ E*2/Δ)
let B := γ/(Real.sqrt (Module.finrank ℝ E*ell)+ell)
let J := Nat.ceil (C*Real.log (Real.exp 1*K s0.1/B))
let D : Set PS := {s | B⁻¹ ≤ (s.1:ℝ)}
∃ T H : Kernel PS E, IsMarkovKernel T ∧ IsMarkovKernel H ∧
(∀ s, T s = μ.tilted (fun x => -((s.1:ℝ)/2)*‖x-s.2.1‖^2)) ∧
(∀ s, H s = GaussianSmoothing.gaussianSmoothing (T s) (Real.sqrt (a s))) ∧
∀ M L : Kernel PS E, IsMarkovKernel M → IsMarkovKernel L →
(∀ s, s ∉ D → WassersteinSpace.wassersteinDistance (M s)
(GaussianSmoothing.gaussianSmoothing (T s) (Real.sqrt (η s/(1+s.1))))^2 ≤
ENNReal.ofReal (K s.1*(2*τ s.1*Δ^2/(K s.1*((J:ℝ)+1)))/(1+s.1))) →
∃ (F : PS × E → PS) (Q : Kernel PS E) (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 Q ∧ IsMarkovKernel P ∧ (∀ n, IsMarkovKernel (R n)) ∧
(∀ s, Q s = GaussianSmoothing.gaussianSmoothing (M s) (Real.sqrt (τ s.1/(1+s.1)))) ∧
(∀ s, P s = if s ∈ D then Measure.dirac s else (Q s).map (fun y => F (s,y))) ∧
(∀ n, R n = L ∘ₖ (P^n)) ∧
0 < B ∧ (P^J) s0 D = 1 ∧
(∀ m, R (J+m) s0 = R J s0) ∧
klDiv (R J s0) (T s0) ≤ (J:ℝ≥0∞)*ENNReal.ofReal (Δ^2/((J:ℝ)+1)) +
∫⁻ x in D, klDiv (L x) (T x) ∂(P^J) s0 ∧
((∀ s ∈ D, klDiv (L s) (T s) ≤ ENNReal.ofReal (Δ^2/((J:ℝ)+1))) →
∀ m, klDiv (R (J+m) s0) (T s0) ≤ ENNReal.ofReal (Δ^2)) := by
classical
have recursive_output_powers (Q L : Kernel (PS) E) [IsMarkovKernel Q] [IsMarkovKernel L]
(F : (PS) × E → (PS)) (hF : Measurable F) (D : Set (PS)) [DecidablePred (· ∈ D)]
(P : Kernel (PS) (PS)) (R : ℕ → Kernel (PS) E)
(hPf : ∀ s, P s = if s ∈ D then Measure.dirac s else (Q s).map (fun y => F (s,y)))
(hzero : R 0 = L)
(hrec : ∀ n s, R (n+1) s = if s ∈ D then L s else (Q s).bind (fun y => R n (F (s,y)))) :
∀ n, R n = L ∘ₖ (P^n) := by
have hstop (n : ℕ) (s : (PS)) (hs : s ∈ D) : R n s = L s := by
cases n with
| zero => rw [hzero]
| succ n => rw [hrec,if_pos hs]
have hRstep (n : ℕ) : R (n+1) = R n ∘ₖ P := by
ext s t ht
rw [Kernel.comp_apply,hPf,hrec]
by_cases hs : s ∈ D
· rw [if_pos hs,if_pos hs,Measure.dirac_bind (R n).measurable,hstop n s hs]
· rw [if_neg hs,if_neg hs]
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
intro n
induction n with
| zero =>
change R 0 = L ∘ₖ Kernel.id
rw [Kernel.comp_id,hzero]
| succ n ih =>
rw [hRstep,ih,pow_succ]
exact Kernel.comp_assoc L (P^n) P
intro K τ a ell B J D
have hb : Measurable (fun s : PS => (s.1:ℝ)) := by fun_prop
have hKm : Measurable (fun s : PS => K s.1) := by dsimp [K]; fun_prop
have hKpos (s : PS) : 0 < K s.1 := by
exact div_pos (by positivity) (add_pos_of_pos_of_nonneg
(inv_pos.mpr (lt_of_lt_of_le zero_lt_one hκ)) s.1.coe_nonneg)
have htm : Measurable (fun s : PS => τ s.1) :=
Measurable.ite (measurableSet_le measurable_const hKm) hKm measurable_const
have htpos (s : PS) : 0 < τ s.1 := by
dsimp [τ]
split_ifs with hs
· linarith
· exact hc
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 (show (2:ℝ) ≤ 2 from le_rfl) hΔ hΔ1 hγ hγ1 hC
change 2 ≤ ell ∧ (0 < B ∧ B ≤ 1) ∧ 0 < J ∧ _ ∧ _ ∧ _ at hdepth
have hB := hdepth.2.1.1
let θ : ℝ≥0 := ⟨B⁻¹,(inv_pos.mpr hB).le⟩
obtain ⟨T,H,hT,hH,hTf,hHf,hprog⟩ :=
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.GaussianRGOErrorBudget.gaussian_rgo_error_budget μ
(fun s : PS => 1+s.1) (fun s : PS => K s.1) η (fun s : PS => τ s.1)
(by fun_prop) hKm hηm htm (fun s => by positivity) hKpos (fun s => (hη s).1.le) htpos θ J Δ hΔ.le
let := hT
let := hH
refine ⟨T,H,hT,hH,hTf,hHf,?_⟩
intro M L hM hL hW
let := hM
let := hL
obtain ⟨F,Q,P,R,hFf,hQ,hP,hR,hQf,hPf,hzero,hrec,hlocal,hbound⟩ := hprog M L hM hL hW
let := hQ
let := hP
obtain ⟨F',P',R',hFf',hP',hR',hPf',hRp',hB',hmass,hstable,hJbound⟩ :=
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.StoppedRGODepth.stopped_rgo_depth μ η hηm κ c 2 Δ γ C
hκ hc hc1 hη hd le_rfl hΔ hΔ1 hγ hγ1 hC s0 Q L
have hFeq : F = F' := by
funext p
apply Prod.ext
· apply Subtype.ext
exact (hFf p.1 p.2).1.trans (hFf' p.1 p.2).1.symm
· exact (hFf p.1 p.2).2.trans (hFf' p.1 p.2).2.symm
subst F'
have hPeq : P = P' := by
ext s t ht
rw [hPf,hPf']
rfl
subst P'
have ha0 (s : PS) : 0 < a s := div_pos (add_pos (hη s).1 (htpos s)) (by positivity)
have hFexact : F = fun p =>
(⟨(p.1.1:ℝ)+(a p.1)⁻¹,add_nonneg p.1.1.coe_nonneg (inv_pos.mpr (ha0 p.1)).le⟩,
((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) := by
funext p
apply Prod.ext
· exact Subtype.ext (hFf p.1 p.2).1
· exact (hFf p.1 p.2).2
have ha : Measurable a := (hηm.add htm).div (by fun_prop)
have hFm : Measurable F := by
rw [hFexact]
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
have hRp : ∀ n, R n = L ∘ₖ (P^n) := recursive_output_powers Q L F hFm D P R hPf hzero hrec
have hReq (n : ℕ) : R n = R' n := (hRp n).trans (hRp' n).symm
have hstable' (m : ℕ) : R (J+m) s0 = R J s0 := by rw [hReq,hReq]; exact hstable m
have hp (n : ℕ) : IsMarkovKernel (P^n) := by
induction n with
| zero => change IsMarkovKernel Kernel.id; infer_instance
| succ n ih =>
let := ih
rw [pow_succ]
change IsMarkovKernel ((P^n) ∘ₖ P)
infer_instance
let := hp J
have hDm : MeasurableSet D := measurableSet_le measurable_const hb
have hae : ∀ᵐ x ∂(P^J) s0, x ∈ D := (mem_ae_iff_prob_eq_one hDm).2 hmass
have hrestrict : ((P^J) s0).restrict D = (P^J) s0 := Measure.restrict_eq_self_of_ae_mem hae
refine ⟨F,Q,P,R,hFf,hQ,hP,hR,hQf,hPf,hRp,hB,hmass,hstable',?_,?_⟩
· rw [hrestrict]
exact hbound J s0
· intro hterminal m
rw [hstable']
apply (hbound J s0).trans
have htbound : (∫⁻ x, klDiv (L x) (T x) ∂(P^J) s0) ≤ ENNReal.ofReal (Δ^2/((J:ℝ)+1)) := by
calc
_ ≤ ∫⁻ x, ENNReal.ofReal (Δ^2/((J:ℝ)+1)) ∂(P^J) s0 := by
apply lintegral_mono_ae
filter_upwards [hae] with x hx
exact hterminal x hx
_ = _ := by simp
calc
_ ≤ (J:ℝ≥0∞)*ENNReal.ofReal (Δ^2/((J:ℝ)+1)) + ENNReal.ofReal (Δ^2/((J:ℝ)+1)) := add_le_add le_rfl htbound
_ = ENNReal.ofReal (Δ^2) := by
rw [← add_one_mul]
rw [← ENNReal.ofReal_natCast,← ENNReal.ofReal_one,← ENNReal.ofReal_add (by positivity) (by positivity),
← ENNReal.ofReal_mul (by positivity)]
congr 1
field_simp
end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.StoppedGaussianRGOErrorScope and omitted-condition boundaries
- M is supplied with the displayed A1 squared-W2 guarantee. The final Delta^2 conclusion additionally assumes terminal KL only on the fixed terminal set. Neither condition is a proof that Picard HMC or FORS implements the interface. The source scalar formulas use baseline smoothness one; no curvature properties of arbitrary mu are established. C>=8 is a proved sufficient depth constant, and gamma in (0,1] is a depth condition, not FORS sufficiency. Initial reference points, history validity and query costs remain open. Threshold and J are fixed using s0; cap stability is a fiber identity at s0. The auxiliary constant-c depth call only proves B>0; actual termination uses StoppedRGODepth. An explicit upper bound on J and measurability of F are not separate public conclusions here.
Source and reuse
ASTIS parents called
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.GaussianRGOErrorBudget.gaussian_rgo_error_budgetAutoSamplingTheory.ExampleCases.SmoothedPicardHMC.StoppedRGODepth.stopped_rgo_depthAutoSamplingTheory.ExampleCases.SmoothedPicardHMC.LogarithmicDepth.terminal_depth
Mathlib API called (external library)
- MeasureTheory.Measure.bind_apply
- MeasureTheory.lintegral_map
- ProbabilityTheory.Kernel.comp_assoc
- MeasureTheory.mem_ae_iff_prob_eq_one
- MeasureTheory.Measure.restrict_eq_self_of_ae_mem
- MeasureTheory.lintegral_mono_ae
Mathematical sources
- SPHMC v1 Theorem 6.5 A1 and equations (6.2)-(6.5) — Same-program stopping and error budget under supplied A1 and terminal KL interfaces.
ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.