Actual Gaussian observation and finite recursive A1 budget
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.GaussianRGOErrorBudget.gaussian_rgo_error_budget · theorem · Teaching coverage
Statement
Let E be a finite-dimensional real inner-product Borel space and mu a probability measure. Set S=NNReal times E times Nat times E^Nat. Let beta,kappa,tau:S to R be positive measurable functions and eta:S to R nonnegative measurable. Fix a nonnegative precision threshold theta, natural budget J and Delta>=0. Define a(s)=(eta(s)+tau(s))/beta(s). 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 with standard deviation sqrt(a(s)). These are chosen before arbitrary Markov smoothed-output M and terminal L. Suppose that on every continuing state, squared W2 from M(s) to T(s) smoothed at time eta(s)/beta(s) is at most ofReal(kappa(s)*[2*tau(s)*Delta^2/(kappa(s)*(J+1))]/beta(s)). Then there exist F,Q,P and Markov output kernels R_n. F updates precision to b+1/a(s), center to (b*u+y/a(s))/(b+1/a(s)), increments the count and prepends y to history. Q(s) is M(s) with an independent Gaussian of variance tau(s)/beta(s) added. P(s)=dirac s if theta<=b and otherwise the F(s,.) pushforward of Q(s). R_0=L, and R_(n+1)(s)=L(s) if stopped, otherwise the bind of Q(s) with R_n(F(s,y)). On every continuing state KL(Q(s)||H(s))<=ofReal(Delta^2/(J+1)). For all n,s, KL(R_n(s)||T(s)) is at most n*ofReal(Delta^2/(J+1)) plus integral KL(L(x)||T(x)) under P^n(s). All bounds are in extended nonnegative reals.
All objects and hypotheses
- Finite-dimensional real Hilbert Borel E, including zero dimension; mu probability.
- beta,kappa,tau are measurable and strictly positive everywhere; eta is measurable and nonnegative. Delta>=0, J natural, theta nonnegative and fixed.
- M,L are measurable Markov kernels on the complete state. Ideal T,H are fixed before their selection.
- Only continuing states require the displayed squared-W2 accuracy with epsilon(s)^2=2*tau(s)*Delta^2/(kappa(s)*(J+1)). No observation KL bound is assumed.
- No stopping bound, terminal accuracy, finite terminal KL, marginal moment or cost-transfer premise is added.
Mathematical proof
1. Construct a measurable actual Gaussian observation kernel
Form the independent product of a deterministic state-retaining kernel and a standard Gaussian kernel, then scale the noise by sqrt(tau(s)/beta(s)). Its fiber is the centered Gaussian at that variance. Take its product with M and push forward by addition. Product and map preserve Markov probability; measurability of the state-dependent scale supplies a single measurable Q, not separately selected fiber measures.
Corresponding Lean step
Local gaussian_kernel; deterministic/constant kernel product, Kernel.map_apply and scaledStdGaussian.
2. Identify the ideal two-noise law
At a fixed state, apply TwoNoiseRGO with times eta/beta and tau/beta to its actual quadratic tilt. The resulting Gaussian semigroup identifies sequential ideal smoothing with the total time (eta+tau)/beta, which equals the H fiber constructed for the finite program. Positivity of beta,tau ensures the added time is strictly positive even when eta=0.
Corresponding Lean step
Local gaussian_stage; TwoNoiseRGO.two_noise_rgo semigroup component, hsem and add_div.
3. Derive the exact per-stage KL allocation from W2
Use the genuine squared-W2 equals quadratic transport-cost identity and set the radius to the square root of the stated nonnegative source budget. GaussianKL compares the actually smoothed laws with denominator twice the added time tau/beta. Substituting equation (6.5) cancels kappa,beta,tau exactly. This needs no separate moment premises and assumes no KL conclusion.
Corresponding Lean step
Local gaussian_stage; wassersteinDistance_sq, Real.sq_sqrt, GaussianKL.gaussian_kl_reverse_transport and field_simp.
4. Instantiate the actual finite recursive program
Use a=(eta+tau)/beta in FiniteRGOKLError. Its ideal target and observation kernels are chosen before M,L. Construct Q as above and instantiate the parent program with this same Q and L, retaining the explicit F, absorbing P and output recursion. The continuing-state W2 premise gives the derived observation-KL bound; stopped states require no W2 guarantee.
Corresponding Lean step
FiniteRGOKLError.finite_rgo_kl_error, gaussian_kernel, hlocal and actual hprog Q L.
5. Integrate the stage bound under actual visited laws
Set observation error to zero on stopped states. It is everywhere bounded by Delta^2/(J+1). Each P^j(s) is a probability measure, so its integral of this error is bounded by the same constant. Sum the n terms and retain the parent terminal integral exactly. The result is valid for any finite n, without claiming threshold arrival at J.
Corresponding Lean step
Main hp, herror and hbound; lintegral_mono, probability normalization and Finset.sum_le_sum.
Lean statement · gaussian_rgo_error_budget
Actual two-noise observation and finite recursive KL budget derived from the source-scaled squared-W2 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 gaussian_rgo_error_budget (μ : Measure E) [IsProbabilityMeasure μ]
(β κ η τ : PS → ℝ) (hβm : Measurable β) (_hκm : Measurable κ)
(hηm : Measurable η) (hτm : Measurable τ)
(hβ : ∀ s, 0 < β s) (hκ : ∀ s, 0 < κ s) (hη : ∀ s, 0 ≤ η s) (hτ : ∀ s, 0 < τ s)
(threshold : ℝ≥0) (J : ℕ) (Δ : ℝ) (_hΔ : 0 ≤ Δ) :
let a := fun s => (η s+τ s)/β s
∃ (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, ¬threshold ≤ s.1 → WassersteinSpace.wassersteinDistance (M s)
(GaussianSmoothing.gaussianSmoothing (T s) (Real.sqrt (η s/β s)))^2 ≤
ENNReal.ofReal (κ s*(2*τ s*Δ^2/(κ s*((J:ℝ)+1)))/β s)) →
∃ (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/β s))) ∧
(∀ s, P s = if threshold ≤ s.1 then Measure.dirac s else (Q s).map (fun y => F (s,y))) ∧
R 0 = L ∧
(∀ n s, R (n+1) s = if threshold ≤ s.1 then L s else (Q s).bind (fun y => R n (F (s,y)))) ∧
(∀ s, ¬threshold ≤ s.1 → klDiv (Q s) (H s) ≤ ENNReal.ofReal (Δ^2/((J:ℝ)+1))) ∧
∀ n s, klDiv (R n s) (T s) ≤
(n:ℝ≥0∞)*ENNReal.ofReal (Δ^2/((J:ℝ)+1)) + ∫⁻ x, klDiv (L x) (T x) ∂(P^n) sLean proof · gaussian_rgo_error_budget
Measurable noise kernel, ideal Gaussian semigroup, source constant cancellation and actual finite-program occupation integral bound.
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 gaussian_rgo_error_budget (μ : Measure E) [IsProbabilityMeasure μ]
(β κ η τ : PS → ℝ) (hβm : Measurable β) (_hκm : Measurable κ)
(hηm : Measurable η) (hτm : Measurable τ)
(hβ : ∀ s, 0 < β s) (hκ : ∀ s, 0 < κ s) (hη : ∀ s, 0 ≤ η s) (hτ : ∀ s, 0 < τ s)
(threshold : ℝ≥0) (J : ℕ) (Δ : ℝ) (_hΔ : 0 ≤ Δ) :
let a := fun s => (η s+τ s)/β s
∃ (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, ¬threshold ≤ s.1 → WassersteinSpace.wassersteinDistance (M s)
(GaussianSmoothing.gaussianSmoothing (T s) (Real.sqrt (η s/β s)))^2 ≤
ENNReal.ofReal (κ s*(2*τ s*Δ^2/(κ s*((J:ℝ)+1)))/β s)) →
∃ (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/β s))) ∧
(∀ s, P s = if threshold ≤ s.1 then Measure.dirac s else (Q s).map (fun y => F (s,y))) ∧
R 0 = L ∧
(∀ n s, R (n+1) s = if threshold ≤ s.1 then L s else (Q s).bind (fun y => R n (F (s,y)))) ∧
(∀ s, ¬threshold ≤ s.1 → klDiv (Q s) (H s) ≤ ENNReal.ofReal (Δ^2/((J:ℝ)+1))) ∧
∀ n s, klDiv (R n s) (T s) ≤
(n:ℝ≥0∞)*ENNReal.ofReal (Δ^2/((J:ℝ)+1)) + ∫⁻ x, klDiv (L x) (T x) ∂(P^n) s := by
classical
have gaussian_kernel {S : Type u} [MeasurableSpace S] (M : Kernel S E) [IsMarkovKernel M]
(v : S → ℝ) (hv : Measurable v) :
∃ Q : Kernel S E, IsMarkovKernel Q ∧
∀ s, Q s = GaussianSmoothing.gaussianSmoothing (M s) (Real.sqrt (v s)) := by
let N : Kernel S E :=
((Kernel.deterministic (id : S → S) measurable_id) ×ₖ Kernel.const S (stdGaussian E)).map
(fun p : S × E => Real.sqrt (v p.1) • p.2)
have hN : IsMarkovKernel N := by
dsimp only [N]
exact Kernel.IsMarkovKernel.map _ (by fun_prop)
let := hN
have hNf (s : S) : N s = GaussianSmoothing.scaledStdGaussian (E := E) (Real.sqrt (v s)) := by
dsimp only [N]
rw [Kernel.map_apply _ (by fun_prop), Kernel.prod_apply, Kernel.deterministic_apply,
Kernel.const_apply, Measure.dirac_prod, Measure.map_map (by fun_prop) (by fun_prop)]
rfl
let Q := (M ×ₖ N).map (fun p : E × E => p.1+p.2)
have hQ : IsMarkovKernel Q := by
dsimp only [Q]
exact Kernel.IsMarkovKernel.map _ (by fun_prop)
refine ⟨Q,hQ,?_⟩
intro s
dsimp only [Q]
rw [Kernel.map_apply _ (by fun_prop), Kernel.prod_apply, hNf]
rfl
have gaussian_stage (μ ν : Measure E) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν]
(b : ℝ) (hb : 0 ≤ b) (u : E) (β κ η τ Δ : ℝ)
(hβ : 0 < β) (hκ : 0 < κ) (hη : 0 ≤ η) (hτ : 0 < τ) (J : ℕ)
(hW : WassersteinSpace.wassersteinDistance ν
(GaussianSmoothing.gaussianSmoothing (μ.tilted (fun x => -(b/2)*‖x-u‖^2)) (Real.sqrt (η/β))) ^ 2 ≤
ENNReal.ofReal (κ * (2*τ*Δ^2/(κ*((J:ℝ)+1))) / β)) :
klDiv (GaussianSmoothing.gaussianSmoothing ν (Real.sqrt (τ/β)))
(GaussianSmoothing.gaussianSmoothing (μ.tilted (fun x => -(b/2)*‖x-u‖^2))
(Real.sqrt ((η+τ)/β))) ≤ ENNReal.ofReal (Δ^2/((J:ℝ)+1)) := by
have hj : 0 < (J:ℝ)+1 := by positivity
have heta : 0 ≤ η/β := div_nonneg hη hβ.le
have htau : 0 < τ/β := div_pos hτ hβ
obtain ⟨hρ,hsem,K,hK,hKf,hrec,herr⟩ :=
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.TwoNoiseRGO.two_noise_rgo μ b (η/β) (τ/β) hb heta htau u
let ρ := μ.tilted (fun x => -(b/2)*‖x-u‖^2)
let := hρ
have hsm : IsProbabilityMeasure (GaussianSmoothing.gaussianSmoothing ρ (Real.sqrt (η/β))) := by
unfold GaussianSmoothing.gaussianSmoothing CommonNoiseContraction.addNoise
exact Measure.isProbabilityMeasure_map (by fun_prop)
let := hsm
let r := Real.sqrt (κ * (2*τ*Δ^2/(κ*((J:ℝ)+1))) / β)
have hrad : 0 ≤ κ * (2*τ*Δ^2/(κ*((J:ℝ)+1))) / β := by positivity
have hr2 : r^2 = κ * (2*τ*Δ^2/(κ*((J:ℝ)+1))) / β := Real.sq_sqrt hrad
have hcost : Transport.transportCost (fun z : E × E => ENNReal.ofReal (‖z.1-z.2‖^2)) ν
(GaussianSmoothing.gaussianSmoothing ρ (Real.sqrt (η/β))) ≤ ENNReal.ofReal (r^2) := by
rw [hr2]
rw [WassersteinSpace.wassersteinDistance_sq] at hW
exact hW
have hg := AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.GaussianKL.gaussian_kl_reverse_transport ν
(GaussianSmoothing.gaussianSmoothing ρ (Real.sqrt (η/β))) r (τ/β)
(Real.sqrt_nonneg _) htau hcost
have hscale : r^2/(2*(τ/β)) = Δ^2/((J:ℝ)+1) := by
rw [hr2]
field_simp
rw [hscale,hsem,← add_div] at hg
exact hg
intro a
have ha : Measurable a := (hηm.add hτm).div hβm
have ha0 : ∀ s, 0 < a s := fun s => div_pos (add_pos_of_nonneg_of_pos (hη s) (hτ s)) (hβ s)
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)
obtain ⟨T,H,hT,hH,hTf,hHf,hprog⟩ :=
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.FiniteRGOKLError.finite_rgo_kl_error μ a ha ha0 threshold
let := hT
let := hH
refine ⟨T,H,hT,hH,hTf,hHf,?_⟩
intro M L hM hL hW
let := hM
let := hL
obtain ⟨Q,hQ,hQf⟩ := gaussian_kernel M (fun s => τ s/β s) (hτm.div hβm)
let := hQ
have hlocal (s : PS) (hs : ¬threshold ≤ s.1) :
klDiv (Q s) (H s) ≤ ENNReal.ofReal (Δ^2/((J:ℝ)+1)) := by
rw [hQf,hHf,hTf]
apply gaussian_stage μ (M s) (s.1:ℝ) s.1.coe_nonneg s.2.1 (β s) (κ s) (η s) (τ s) Δ
(hβ s) (hκ s) (hη s) (hτ s) J
simpa only [hTf] using hW s hs
obtain ⟨P,R,hP,hR,hPf,hzero,hrec,he,ht,hbound⟩ := hprog Q L hQ hL
let := hP
refine ⟨F,Q,P,R,?_,hQ,hP,hR,hQf,hPf,hzero,hrec,hlocal,?_⟩
· intro s y
exact ⟨rfl,rfl⟩
· 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
have herror (x : PS) : (if threshold ≤ x.1 then 0 else klDiv (Q x) (H x)) ≤
ENNReal.ofReal (Δ^2/((J:ℝ)+1)) := by
split_ifs with hs
· positivity
· exact hlocal x hs
intro n s
apply (hbound n s).trans
apply add_le_add _ le_rfl
calc
_ ≤ ∑ j ∈ Finset.range n, ENNReal.ofReal (Δ^2/((J:ℝ)+1)) := by
apply Finset.sum_le_sum
intro j hj
exact (lintegral_mono herror).trans_eq (by simp)
_ = _ := by simp
end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.GaussianRGOErrorBudgetScope and omitted-condition boundaries
- M is a supplied Markov kernel satisfying the displayed squared-W2 guarantee; its implementation and A1 correctness are not proved here. beta,kappa,tau are positive measurable algebraic functions, not yet identified with source curvature and heat choices. kappa measurability is an unused input condition, not a proved precision-selection implementation. eta may be zero, Delta is nonnegative, J may be zero, and n is unrestricted. J is a budget parameter: for n>J this bound does not establish total error below Delta^2. No stopping support, FORS accuracy, initialization validity, expected query cost or marginal P2 conclusion is asserted; the terminal residual remains.
Source and reuse
ASTIS parents called
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.FiniteRGOKLError.finite_rgo_kl_errorAutoSamplingTheory.ExampleCases.SmoothedPicardHMC.TwoNoiseRGO.two_noise_rgoAutoSamplingTheory.ExampleCases.SmoothedPicardHMC.GaussianKL.gaussian_kl_reverse_transport
Mathlib API called (external library)
- ProbabilityTheory.Kernel.map_apply
- MeasureTheory.Measure.dirac_prod
- WassersteinSpace.wassersteinDistance_sq
- MeasureTheory.lintegral_mono
- Finset.sum_le_sum
Mathematical sources
- SPHMC v1 Theorem 6.5 A1 and equation (6.5) — Actual added-noise kernel and numerical error transfer from supplied A1 accuracy; no concrete sampler or terminal-cost result.
ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.