Actual proximal Gaussian estimator and its fiberwise moments
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ProximalGaussianEstimator.proximal_gaussian_estimator · theorem · Teaching coverage
Mathematical 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.
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 ℝ EProof roadmap
- 1Derive 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.
- 2Construct 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.
- 3Identify 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.
- 4Prove 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.
- 5Establish 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.
- 6Prove 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.
- 7Construct 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.
- 8Transfer 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.
Full assumptions and notation
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 verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean 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.ProximalGaussianEstimatorSource assumptions versus formal assumptions
| Source | Actual Lean | Difference kind | Why it matters |
|---|---|---|---|
| Source is Euclidean with positive dimension and explicit C2/Hessian bounds. | Coordinate-free finite-dimensional real inner-product Borel space,including zero dimension; same genuine C2/Hessian bounds. | generalization | Zero dimension and coordinate-free presentation are extensions;C2 agrees with source(1.1). |
| Source estimator is evaluated at algorithmic random centers and step sizes. | Any measurable S and measurable eta,y;no topology or probability law on S. | generalization | The parameterized theorem can consume actual random centers without assuming a measurable proximal selection; no topology or probability law on S is needed. |
| Equation(3.2) uses the exact proximal oracle. | The constructed point satisfies the actual proximal equation and unique global minimum. | same | This identifies the same exact oracle mathematically; a finite gradient evaluator is not supplied. |
| The paper normalizes beta=1 and kappa>=1 in this analysis. | Both remain explicit hypotheses;the kappa>=1 binder is unused in the proof. | same | An unused proof hypothesis is still part of the public theorem and is not silently removed. |
| Later estimator analysis controls error relative to the actual smoothed score. | Deviation second moment is centered at gradient V(p),not the estimator mean or smoothed score. | API-limitation | Neither variance about the estimator mean nor Lemma4.2 score bias is claimed. |
| Full algorithms use random states and charge oracle implementation costs. | Only fiberwise L2 and moments of the exact oracle;no state-law integral or gradient evaluator trace. | API-limitation | Global state moments,Picard output accuracy,initialization and total costs remain separate. |
| The proximal estimator formula is meaningful for positive smoothing parameters;the algorithm selects small parameters. | The public construction assumes0<eta_s<=1/2. | API-limitation | The bound1/2 is a sufficient contraction condition of this construction,not a claimed optimal source threshold. An algorithm consumer must establish this bound for its actual parameters;the theorem does not cover every positive eta. |
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.
Encoder–denoiser: accepted · domain-mismatch
Detected semantic differences
- domains: Coordinate-free and zero-dimensional domain extension. — Independent formal source reviewer accepted: Coordinate-free and zero-dimensional domain extension.
- domains: Arbitrary measurable parameter space extension. — Independent formal source reviewer accepted: Arbitrary measurable parameter space extension.
- objects: Same exact proximal oracle,not a finite gradient evaluator. — Independent formal source reviewer accepted: Same exact proximal oracle,not a finite gradient evaluator.
- assumptions: Beta1 and kappa>=1 retained,including unused public inequality. — Independent formal source reviewer accepted: Beta1 and kappa>=1 retained,including unused public inequality.
- conclusion: Deviation center is not estimator mean or smoothed score. — Independent formal source reviewer accepted: Deviation center is not estimator mean or smoothed score.
- scopes: Fiber moments and exact-oracle boundary exclude global state moments and costs. — Independent formal source reviewer accepted: Fiber moments and exact-oracle boundary exclude global state moments and costs.
- assumptions: Eta<=1/2 sufficient domain,not an optimal existence threshold. — Independent formal source reviewer accepted: Eta<=1/2 sufficient domain,not an optimal existence threshold.
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
- 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.
Sources, dependencies, and reuse
Source and reuse
Samplinglib 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.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.