Actual proximal Gaussian estimator and its fiberwise moments
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ProximalGaussianEstimator.proximal_gaussian_estimator · theorem · Teaching coverage
Statement
There exists a measurable p:S->E such that p_s+eta_s*gradient V(p_s)=y_s. For all s,z,F_s(p_s)+(kappa^(-1)+eta_s^(-1))*norm(z-p_s)^2/2<=F_s(z),and F_s(z)<=F_s(p_s) if and only if z=p_s. Set G(s,z)=gradient V(p_s+sqrt(eta_s)*z). G is jointly measurable. There exists a Markov kernel K:S->E whose fiber is exactly StandardGaussian(E).map(z->G(s,z)). For every s,both G(s,.) and G(s,.)-gradient V(p_s) belong to L2(StandardGaussian(E)); the integral of norm(G(s,z)-gradient V(p_s))^2 is at most eta_s*d,and the integral of norm(G(s,z))^2 is at most 2*norm(gradient V(p_s))^2+2*eta_s*d. Finally norm(w)^2 is integrable under the actual K_s,and its K_s integral satisfies that same total second-moment bound.
All objects and hypotheses
- E is a finite-dimensional real inner-product Borel space with its complete metric structure; d=dim_R E may be zero. S is any measurable space,with no topology,standard Borel hypothesis or probability law required.
- The nonnegative real kappa satisfies kappa>=1. V:E->R is C2 and kappa^(-1)*norm(v)^2<=D2V(x)[v,v]<=norm(v)^2 for every x,v. The normalization is beta=1. Kappa>=1 remains an explicit hypothesis although the proof does not use that inequality.
- eta:S->R and y:S->E are measurable,with 0<eta_s<=1/2 for every s. No uniform positive lower bound on eta is assumed. Define F_s(x)=V(x)+norm(x-y_s)^2/(2 eta_s).
- gradient V is the genuine real inner-product gradient,defined through the Frechet derivative. StandardGaussian(E) has zero mean and identity covariance; in zero dimension it is the Dirac law at zero. All displayed real integrals are Bochner integrals and all asserted L2 properties are with respect to this actual Gaussian law or the specified kernel fiber.
Mathematical proof
1. Derive actual gradient Lipschitzness
Use the genuine source Hessian bounds in QuadraticRegularization with zero added precision. This proves the real gradient is 1-Lipschitz; no abstract replacement gradient or supplied Lipschitz premise enters the public theorem.
Corresponding Lean step
actual_proximal_minimizer: hLip; proximal_gaussian_estimator: hHprime,hLip
2. Construct one measurable proximal point
For every parameter define f_s(x)=y_s-eta_s*gradient V(x). Its Lipschitz constant is at most1/2. Banach contraction constructs p_s. Iterates from the common zero vector are measurable in s by induction; pointwise convergence and the measurable-limit theorem prove the measurability of this same p. The fixed point equation is then rearranged.
Corresponding Lean step
parameterized_contraction_point: f,hc,p,hit,hp,heq
3. Identify the true regularized gradient
Differentiate the squared norm after translation and add the genuine derivative of V. The proximal equation and eta_s nonzero give gradient F_s(p_s)=0. This uses the actual potential F_s,not a supplied stationary-point certificate.
Corresponding Lean step
actual_proximal_minimizer: hd,hq,hFd,hg,hz
4. Prove global quadratic growth and unique minimality
QuadraticRegularization gives curvature m+eta_s inverse,where m=kappa inverse. StrongConvexFirstOrder at the actual stationary point gives the global quadratic lower bound. Its coefficient is strictly positive because eta_s>0,even for the internal helper m=0. If any point has no larger objective value,the squared displacement must vanish. This supplies unique argmin,not merely fixed-point uniqueness.
Corresponding Lean step
actual_proximal_minimizer: hsc,hbound,ha,hnonpos,hn
5. Establish the actual Gaussian square moment
The Gaussian L2 identity gives norm-square integrability. In a finite orthonormal basis,the covariance identity and zero mean give unit second moment in each coordinate. Parseval and a justified finite integral sum yield total moment d,including the empty sum in zero dimension. This adapts the private gaussian_square proof in ApproximateInitialGradientMoment without claiming a public theorem call.
Corresponding Lean step
gaussian_square: hi,b,hdir,hL1
6. Prove integrability before comparing estimator moments
For fixed p and positive eta,the genuine Lipschitz estimate bounds the squared deviation from gradient V(p) by eta*norm(z)^2. This integrable Gaussian majorant proves square L1 before integration. The triangle inequality gives total square at most2*norm(gradient V(p))^2+2*eta*norm(z)^2;its own integrable majorant then proves the total bound. This is not a variance or smoothed-score bias assertion.
Corresponding Lean step
actual_gaussian_gradient_moments: hG,hb,hs,hdom,hi,hint,ht,hdom2,hi2
7. Construct the actual parameter kernel
Joint measurability follows by composing the continuous gradient with measurable p,eta and the noise coordinate. Form the product of the identity kernel on S and the constant standard Gaussian kernel,then map by this actual G. The Markov map theorem gives probability fibers. Dirac-product and pushforward composition identify each fiber exactly with the Gaussian estimator law.
Corresponding Lean step
proximal_gaussian_estimator: G,hG,K,hK,hKs
8. Transfer the proved moments to the actual output law
Apply the fixed-parameter moment proof to the same actual gradient and proximal point. Joint measurability restricts to measurable Gaussian fibers and deviations. The L2 characterization turns the square-integrability results into both MemLp conclusions. The exact fiber identity,integrable-map theorem and integral-map theorem transfer norm-square L1 and its bound to K_s. No integration over a state distribution is taken.
Corresponding Lean step
proximal_gaussian_estimator: hm,hGs,hdev,hiK,hintK
Lean statement · proximal_gaussian_estimator
Same measurable exact proximal point,quantitative unique argmin,actual Gaussian estimator and Markov kernel,fiberwise L2 and second moments.
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 proximal_gaussian_estimator
{E S : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
[CompleteSpace E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
[MeasurableSpace S] {V : E → ℝ} {κ : ℝ≥0} (_hκ : 1 ≤ κ)
(hV : ContDiff ℝ 2 V)
(hH : ∀ x v : E, (κ:ℝ)⁻¹*‖v‖^2 ≤ (fderiv ℝ (fderiv ℝ V) x v) v ∧
(fderiv ℝ (fderiv ℝ V) x v) v ≤ ‖v‖^2)
{eta : S → ℝ} {y : S → E} (heta : Measurable eta) (hy : Measurable y)
(hpos : ∀ s, 0 < eta s) (hsmall : ∀ s, eta s ≤ 1/2) :
let F := fun s x => V x + (eta s)⁻¹/2*‖x-y s‖^2
∃ p : S → E, Measurable p ∧
(∀ s, p s + eta s • gradient V (p s) = y s) ∧
(∀ s z, F s (p s) + ((κ:ℝ)⁻¹+(eta s)⁻¹)/2*‖z-p s‖^2 ≤ F s z ∧
(F s z ≤ F s (p s) ↔ z=p s)) ∧
let G := fun q : S × E => gradient V (p q.1+Real.sqrt (eta q.1) • q.2)
Measurable G ∧ ∃ K : Kernel S E, IsMarkovKernel K ∧
(∀ s, K s = (stdGaussian E).map (fun z => G (s,z))) ∧
∀ s, MemLp (fun z => G (s,z)) 2 (stdGaussian E) ∧
MemLp (fun z => G (s,z)-gradient V (p s)) 2 (stdGaussian E) ∧
(∫ z, ‖G (s,z)-gradient V (p s)‖^2 ∂stdGaussian E) ≤ eta s*Module.finrank ℝ E ∧
(∫ z, ‖G (s,z)‖^2 ∂stdGaussian E) ≤ 2*‖gradient V (p s)‖^2+2*eta s*Module.finrank ℝ E ∧
Integrable (fun w : E => ‖w‖^2) (K s) ∧
(∫ w : E, ‖w‖^2 ∂K s) ≤ 2*‖gradient V (p s)‖^2+2*eta s*Module.finrank ℝ ELean proof · proximal_gaussian_estimator
Uniform contraction and measurable limit;true regularized gradient and strong convexity;Gaussian moments and integrable domination;actual kernel pushforward and integral transfer.
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 proximal_gaussian_estimator
{E S : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
[CompleteSpace E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
[MeasurableSpace S] {V : E → ℝ} {κ : ℝ≥0} (_hκ : 1 ≤ κ)
(hV : ContDiff ℝ 2 V)
(hH : ∀ x v : E, (κ:ℝ)⁻¹*‖v‖^2 ≤ (fderiv ℝ (fderiv ℝ V) x v) v ∧
(fderiv ℝ (fderiv ℝ V) x v) v ≤ ‖v‖^2)
{eta : S → ℝ} {y : S → E} (heta : Measurable eta) (hy : Measurable y)
(hpos : ∀ s, 0 < eta s) (hsmall : ∀ s, eta s ≤ 1/2) :
let F := fun s x => V x + (eta s)⁻¹/2*‖x-y s‖^2
∃ p : S → E, Measurable p ∧
(∀ s, p s + eta s • gradient V (p s) = y s) ∧
(∀ s z, F s (p s) + ((κ:ℝ)⁻¹+(eta s)⁻¹)/2*‖z-p s‖^2 ≤ F s z ∧
(F s z ≤ F s (p s) ↔ z=p s)) ∧
let G := fun q : S × E => gradient V (p q.1+Real.sqrt (eta q.1) • q.2)
Measurable G ∧ ∃ K : Kernel S E, IsMarkovKernel K ∧
(∀ s, K s = (stdGaussian E).map (fun z => G (s,z))) ∧
∀ s, MemLp (fun z => G (s,z)) 2 (stdGaussian E) ∧
MemLp (fun z => G (s,z)-gradient V (p s)) 2 (stdGaussian E) ∧
(∫ z, ‖G (s,z)-gradient V (p s)‖^2 ∂stdGaussian E) ≤ eta s*Module.finrank ℝ E ∧
(∫ z, ‖G (s,z)‖^2 ∂stdGaussian E) ≤ 2*‖gradient V (p s)‖^2+2*eta s*Module.finrank ℝ E ∧
Integrable (fun w : E => ‖w‖^2) (K s) ∧
(∫ w : E, ‖w‖^2 ∂K s) ≤ 2*‖gradient V (p s)‖^2+2*eta s*Module.finrank ℝ E := by
let F := fun s x => V x + (eta s)⁻¹/2*‖x-y s‖^2
have hH' : ∀ x v : E, ((κ⁻¹:ℝ≥0):ℝ)*‖v‖^2 ≤ (fderiv ℝ (fderiv ℝ V) x v) v ∧
(fderiv ℝ (fderiv ℝ V) x v) v ≤ (1:ℝ≥0)*‖v‖^2 := by
simpa only [NNReal.coe_inv,NNReal.coe_one,one_mul] using hH
obtain ⟨p,hp,heq,hmin⟩ := actual_proximal_minimizer hV hH' heta hy hpos hsmall
have hLip : LipschitzWith 1 (gradient V) := by
have hb := AutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticRegularization.strongConvexOn_and_lipschitzWith_gradient_add_quadratic (r := 0) hV hH' (0:E)
simpa using hb.2
refine ⟨p,hp,heq,?_,?_⟩
· simpa only [NNReal.coe_inv] using hmin
let G := fun q : S × E => gradient V (p q.1+Real.sqrt (eta q.1) • q.2)
have hG : Measurable G := hLip.continuous.measurable.comp
((hp.comp measurable_fst).add ((heta.comp measurable_fst).sqrt.smul measurable_snd))
let K := (Kernel.id ×ₖ Kernel.const S (stdGaussian E)).map G
have hK : IsMarkovKernel K := Kernel.IsMarkovKernel.map _ hG
have hKs (s : S) : K s = (stdGaussian E).map (fun z => G (s,z)) := by
dsimp only [K]
rw [Kernel.map_apply _ hG,Kernel.prod_apply,Kernel.id_apply,Kernel.const_apply,
Measure.dirac_prod,Measure.map_map hG (by fun_prop)]
rfl
refine ⟨hG,K,hK,hKs,fun s => ?_⟩
have hm := actual_gaussian_gradient_moments hLip (p s) (hpos s)
change Integrable (fun z => ‖G (s,z)-gradient V (p s)‖^2) (stdGaussian E) ∧
(∫ z, ‖G (s,z)-gradient V (p s)‖^2 ∂stdGaussian E) ≤ eta s*Module.finrank ℝ E ∧
Integrable (fun z => ‖G (s,z)‖^2) (stdGaussian E) ∧
(∫ z, ‖G (s,z)‖^2 ∂stdGaussian E) ≤ 2*‖gradient V (p s)‖^2+2*eta s*Module.finrank ℝ E at hm
have hGs : Measurable (fun z => G (s,z)) := hG.comp (measurable_const.prodMk measurable_id)
have hdev : Measurable (fun z => G (s,z)-gradient V (p s)) := hGs.sub measurable_const
have hiK : Integrable (fun w : E => ‖w‖^2) (K s) := by
rw [hKs]
exact (integrable_map_measure (by fun_prop) hGs.aemeasurable).2 hm.2.2.1
have hintK : (∫ w : E, ‖w‖^2 ∂K s) = ∫ z, ‖G (s,z)‖^2 ∂stdGaussian E := by
rw [hKs]
exact integral_map hGs.aemeasurable (by fun_prop)
refine ⟨(memLp_two_iff_integrable_sq_norm hGs.aestronglyMeasurable).2 hm.2.2.1,
(memLp_two_iff_integrable_sq_norm hdev.aestronglyMeasurable).2 hm.1,
hm.2.1,hm.2.2.2,hiK,?_⟩
rw [hintK]
exact hm.2.2.2
end
end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ProximalGaussianEstimatorScope and omitted-condition boundaries
- Actual exact proximal Gaussian gradient estimator from source(3.2), with normalized beta=1,kappa>=1,C2 and genuine Hessian bounds. Arbitrary measurable parameter spaces and zero-dimensional finite inner-product Borel spaces are explicit extensions. Step sizes are measurable and in(0,1/2],without a uniform positive lower bound. The same constructed measurable proximal point supplies the true gradient estimator and exact Markov pushforward. Squared deviation is about gradient V(p),not estimator variance about its mean or error relative to the smoothed score. All L2 and moment conclusions are fiberwise; no arbitrary state-law integrability is inferred. No finite gradient evaluator trace or query count,score bias,Picard updates,stage W2 accuracy,initialization/total cost or full main result is claimed.
Source and reuse
ASTIS parents called
AutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticRegularization.strongConvexOn_and_lipschitzWith_gradient_add_quadraticAutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexFirstOrder.firstOrder_lower_bound_of_strongConvexOn
Mathlib API called (external library)
- ContractingWith.fixedPoint
- ContractingWith.tendsto_iterate_fixedPoint
- measurable_of_tendsto_metrizable
- ProbabilityTheory.covarianceBilin_stdGaussian
- MeasureTheory.memLp_two_iff_integrable_sq_norm
- ProbabilityTheory.Kernel.IsMarkovKernel.map
- MeasureTheory.integrable_map_measure
- MeasureTheory.integral_map
Mathematical sources
- SPHMC(3.2) and Algorithm3.1 — Actual exact proximal Gaussian gradient estimator from source(3.2), with normalized beta=1,kappa>=1,C2 and genuine Hessian bounds. Arbitrary measurable parameter spaces and zero-dimensional finite inner-product Borel spaces are explicit extensions. Step sizes are measurable and in(0,1/2],without a uniform positive lower bound. The same constructed measurable proximal point supplies the true gradient estimator and exact Markov pushforward. Squared deviation is about gradient V(p),not estimator variance about its mean or error relative to the smoothed score. All L2 and moment conclusions are fiberwise; no arbitrary state-law integrability is inferred. No finite gradient evaluator trace or query count,score bias,Picard updates,stage W2 accuracy,initialization/total cost or full main result is claimed.
ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.