Actual proximal estimator: stability in both inputs

Samplinglib exposition of Fan Chen, Sinho Chewi, Jianfeng Lu and Matthew S. Zhang's input-stability estimates; an explicitly restricted constructed-oracle proof component, not the full lemma.

Complete source statement (Samplinglib restatement)

There exists a measurable map p:E→E with p(y)+eta∇V(p(y))=y. For every y,z it satisfies F_y(p(y))+((kappa^-1+eta^-1)/2)||z-p(y)||² <= F_y(z), and F_y(z)<=F_y(p(y)) iff z=p(y). The map p is 1-Lipschitz. For the actual estimator ĝ_eta(y;G)=∇V(p(y)+sqrt(eta)G), the position-input difference is at most ||y-y'|| and the noise-input difference is at most sqrt(eta)||G-G'||.

Pointwise input stability

Read the formalized proofs

Each statement and proof below has its own closed Lean disclosure. Samplinglib parents, Mathlib calls and external mathematical sources are distinguished in each proof.

Samplinglib mathematical lesson

Actual proximal estimator: stability in both inputs

AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ProximalEstimatorLipschitz.proximal_estimator_lipschitz · theorem · Teaching coverage

Read this first

Mathematical statement

There exists a measurable map p:E→E with p(y)+eta∇V(p(y))=y. For every y,z it satisfies F_y(p(y))+((kappa^-1+eta^-1)/2)||z-p(y)||² ≤ F_y(z), and F_y(z)≤F_y(p(y)) iff z=p(y). The map p is 1-Lipschitz. For the actual estimator ĝ_eta(y;G)=∇V(p(y)+sqrt(eta)G), the position-input difference is at most ||y-y'|| and the noise-input difference is at most sqrt(eta)||G-G'||.

\[\widehat g_\eta(y;G)=\nabla V(p(y)+\sqrt\eta G),\quad\|\widehat g_\eta(y;G)-\widehat g_\eta(y';G)\|\le\|y-y'\|,\quad\|\widehat g_\eta(y;G)-\widehat g_\eta(y;G')\|\le\sqrt\eta\|G-G'\|.\]

Lean statement · proximal_estimator_lipschitz

The code below supplies the full constructed map, exact optimality/minimum certificate, and both pointwise bounds with all typeclasses explicit.

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.

Download module (.lean)

theorem proximal_estimator_lipschitz
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [CompleteSpace E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {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 : ℝ} (hpos : 0 < eta) (hsmall : eta ≤ 1 / 2) :
    let F := fun y x => V x + eta⁻¹ / 2 * ‖x - y‖ ^ 2
    ∃ p : E → E, Measurable p ∧
      (∀ y, p y + eta • gradient V (p y) = y) ∧
      (∀ y z, F y (p y) + ((κ : ℝ)⁻¹ + eta⁻¹) / 2 * ‖z - p y‖ ^ 2 ≤ F y z ∧
        (F y z ≤ F y (p y) ↔ z = p y)) ∧
      LipschitzWith 1 p ∧
      (∀ y y' G, ‖gradient V (p y + Real.sqrt eta • G) -
        gradient V (p y' + Real.sqrt eta • G)‖ ≤ ‖y - y'‖) ∧
      (∀ y G G', ‖gradient V (p y + Real.sqrt eta • G) -
        gradient V (p y + Real.sqrt eta • G')‖ ≤ Real.sqrt eta * ‖G - G'‖)

Exact module and namespace context

Proof roadmap

1Construct the same exact proximal oracle
Specialize the existing parameterized theorem to identity centers and constant eta. Retain the actual optimality equation, measurability and quantitative unique-minimum certificate; do not choose a new arbitrary function called a proximal map. The parent constructs it as a limit of contracting iterations. Its Gaussian moments are not new results here.
2Turn genuine Hessian bounds into gradient controls
Apply the existing quadratic-regularization result with zero added precision. This produces strong convexity and 1-Lipschitz gradient from the actual C2 Hessian. Apply the existing two-point first-order bound to this genuine gradient. Its nonnegative lower bound gives monotonicity.
3Subtract optimality and pair with the displacement
Let d=p(y)-p(y') and e=∇V(p(y))-∇V(p(y')). Subtract the actual equations. Pair with d. Nonnegative eta and gradient monotonicity make the added term nonnegative. This is the shared resolvent step extracted from this existing proof, with no new mathematical-completion credit, not a supplied nonexpansiveness assumption.
4Apply Cauchy-Schwarz and cancel only when permitted
Cauchy-Schwarz bounds the pairing by ||y-y'|| ||d||. If d=0 the required inequality is immediate. Otherwise ||d||>0 and cancellation gives the result. This step covers zero-dimensional spaces too. The extracted shared argument only needs eta≥0; the public construction has a narrower range.
5Hold the noise fixed and compare centers
Use the 1-Lipschitz genuine gradient. The common translated noise cancels from its two arguments; then apply nonexpansiveness of p. Every G is allowed, so this pathwise inequality can later be used under shared random noise.
6Hold the center fixed and compare noise inputs
Again apply the gradient Lipschitz bound. The common proximal point cancels, scalar multiplication distributes over subtraction, and sqrt(eta) is nonnegative. No expectation, Gaussian concentration, integrability or smoothed-score identity is needed or established.

Full assumptions and notation

All objects and hypotheses

E is a finite-dimensional complete real inner-product space with its Borel sigma algebra; dimension zero is allowed.
V:E→R is genuinely twice continuously Frechet differentiable; kappa is a nonnegative real with kappa≥1. For every x,v, kappa^-1 ||v||^2 ≤ D²V(x)[v,v] ≤ ||v||^2 (normalized beta=1).
Fix 0<eta≤1/2. Set F_y(x)=V(x)+||x-y||²/(2 eta). All y,y',G,G' are arbitrary deterministic vectors. No Gaussian-law or integrability hypothesis is used for these pointwise inequalities.

Mathematical proof

1. Construct the same exact proximal oracle

Specialize the existing parameterized theorem to identity centers and constant eta. Retain the actual optimality equation, measurability and quantitative unique-minimum certificate; do not choose a new arbitrary function called a proximal map. The parent constructs it as a limit of contracting iterations. Its Gaussian moments are not new results here.

\[p(y)+\eta\nabla V(p(y))=y,\qquad F_y(z)\ge F_y(p(y))+\tfrac{\kappa^{-1}+\eta^{-1}}2\|z-p(y)\|^2.\]

Corresponding Lean step

obtain p,hp,heq,hmin from ProximalGaussianEstimator.proximal_gaussian_estimator

2. Turn genuine Hessian bounds into gradient controls

Apply the existing quadratic-regularization result with zero added precision. This produces strong convexity and 1-Lipschitz gradient from the actual C2 Hessian. Apply the existing two-point first-order bound to this genuine gradient. Its nonnegative lower bound gives monotonicity.

\[\|\nabla V(a)-\nabla V(b)\|\le\|a-b\|,\qquad\langle\nabla V(a)-\nabla V(b),a-b\rangle\ge\kappa^{-1}\|a-b\|^2\ge0.\]

Corresponding Lean step

hH',hreg,hLip,hsc,hmono; DifferentiableAt.hasGradientAt

3. Subtract optimality and pair with the displacement

Let d=p(y)-p(y') and e=∇V(p(y))-∇V(p(y')). Subtract the actual equations. Pair with d. Nonnegative eta and gradient monotonicity make the added term nonnegative. This is the shared resolvent step extracted from this existing proof, with no new mathematical-completion credit, not a supplied nonexpansiveness assumption.

\[y-y'=d+\eta e,\qquad\langle y-y',d\rangle=\|d\|^2+\eta\langle e,d\rangle\ge\|d\|^2.\]

Corresponding Lean step

MonotoneProximalMap.nonexpansive_of_monotone_optimality: hsub,hpair

4. Apply Cauchy-Schwarz and cancel only when permitted

Cauchy-Schwarz bounds the pairing by ||y-y'|| ||d||. If d=0 the required inequality is immediate. Otherwise ||d||>0 and cancellation gives the result. This step covers zero-dimensional spaces too. The extracted shared argument only needs eta≥0; the public construction has a narrower range.

\[\|d\|^2\le\|y-y'\|\|d\|\quad\Longrightarrow\quad\|p(y)-p(y')\|\le\|y-y'\|.\]

Corresponding Lean step

MonotoneProximalMap.nonexpansive_of_monotone_optimality; hpLip

5. Hold the noise fixed and compare centers

Use the 1-Lipschitz genuine gradient. The common translated noise cancels from its two arguments; then apply nonexpansiveness of p. Every G is allowed, so this pathwise inequality can later be used under shared random noise.

\[\|\widehat g_\eta(y;G)-\widehat g_\eta(y';G)\|\le\|(p(y)+\sqrt\eta G)-(p(y')+\sqrt\eta G)\|=\|p(y)-p(y')\|\le\|y-y'\|.\]

Corresponding Lean step

first final branch: hLip.dist_le_mul,hpLip.dist_le_mul,add_sub_add_right_eq_sub

6. Hold the center fixed and compare noise inputs

Again apply the gradient Lipschitz bound. The common proximal point cancels, scalar multiplication distributes over subtraction, and sqrt(eta) is nonnegative. No expectation, Gaussian concentration, integrability or smoothed-score identity is needed or established.

\[\|\widehat g_\eta(y;G)-\widehat g_\eta(y;G')\|\le\|\sqrt\eta(G-G')\|=\sqrt\eta\|G-G'\|.\]

Corresponding Lean step

second final branch: hLip.dist_le_mul,smul_sub,norm_smul,Real.sqrt_nonneg

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · proximal_estimator_lipschitz

Existing proximal construction and genuine Hessian APIs; monotone optimality pairing; Cauchy-Schwarz with a zero case; two translation and scalar norm estimates.

Download module (.lean)

theorem proximal_estimator_lipschitz
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [CompleteSpace E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {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 : ℝ} (hpos : 0 < eta) (hsmall : eta ≤ 1 / 2) :
    let F := fun y x => V x + eta⁻¹ / 2 * ‖x - y‖ ^ 2
    ∃ p : E → E, Measurable p ∧
      (∀ y, p y + eta • gradient V (p y) = y) ∧
      (∀ y z, F y (p y) + ((κ : ℝ)⁻¹ + eta⁻¹) / 2 * ‖z - p y‖ ^ 2 ≤ F y z ∧
        (F y z ≤ F y (p y) ↔ z = p y)) ∧
      LipschitzWith 1 p ∧
      (∀ y y' G, ‖gradient V (p y + Real.sqrt eta • G) -
        gradient V (p y' + Real.sqrt eta • G)‖ ≤ ‖y - y'‖) ∧
      (∀ y G G', ‖gradient V (p y + Real.sqrt eta • G) -
        gradient V (p y + Real.sqrt eta • G')‖ ≤ Real.sqrt eta * ‖G - G'‖) := by
  obtain ⟨p, hp, heq, hmin, _⟩ :=
    ProximalGaussianEstimator.proximal_gaussian_estimator hκ hV hH
      (eta := fun _ : E => eta) (y := id) measurable_const measurable_id
      (fun _ => hpos) (fun _ => hsmall)
  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
  have hreg :=
    AutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticRegularization.strongConvexOn_and_lipschitzWith_gradient_add_quadratic
      (r := 0) hV hH' (0 : E)
  have hLip : LipschitzWith 1 (gradient V) := by simpa using hreg.2
  have hsc : StrongConvexOn Set.univ ((κ : ℝ)⁻¹) V := by simpa using hreg.1
  have hmono (x y : E) : 0 ≤ inner ℝ (gradient V x - gradient V y) (x - y) := by
    have hb :=
      AutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexFirstOrder.gradient_inner_lower_bound_of_strongConvexOn hsc
          (fun z _ => (hV.differentiable (by norm_num) z).hasGradientAt)
          (x := y) (y := x) (Set.mem_univ _) (Set.mem_univ _)
    exact (mul_nonneg (inv_nonneg.mpr (NNReal.coe_nonneg κ)) (sq_nonneg _)).trans hb
  have hpLip := TechnicalLemmas.Analysis.MonotoneProximalMap.nonexpansive_of_monotone_optimality hpos.le hmono heq
  refine ⟨p, hp, heq, hmin, hpLip, ?_, ?_⟩
  · intro y y' G
    have hg := hLip.dist_le_mul (p y + Real.sqrt eta • G) (p y' + Real.sqrt eta • G)
    have hy := hpLip.dist_le_mul y y'
    simp only [NNReal.coe_one, one_mul, dist_eq_norm, add_sub_add_right_eq_sub] at hg hy
    exact hg.trans hy
  · intro y G G'
    have hg := hLip.dist_le_mul (p y + Real.sqrt eta • G) (p y + Real.sqrt eta • G')
    simpa only [NNReal.coe_one, one_mul, dist_eq_norm, add_sub_add_left_eq_sub,
      ← smul_sub, norm_smul, Real.norm_eq_abs, abs_of_nonneg (Real.sqrt_nonneg eta)] using hg

end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ProximalEstimatorLipschitz

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
Source uses R^d.	E is a finite-dimensional complete real inner-product space with its Borel sigma algebra; dimension zero is allowed.	generalization	Coordinate-free finite-dimensional argument includes the zero-dimensional case, not an infinite-dimensional claim.
Normalized C2 potential with Hessian between kappa^-1 and1, kappa>=1.	V:E→R is genuinely twice continuously Frechet differentiable; kappa is a nonnegative real with kappa>=1. For every x,v, kappa^-1 \|\|v\|\|^2 <= D²V(x)[v,v] <= \|\|v\|\|^2 (normalized beta=1).	same	ContDiff guarantees genuine derivatives; totalized gradient values are not substituted for differentiability.
The two pointwise estimates are not limited by a eta<=1/2 threshold.	0<eta<=1/2.	API-limitation	Inherited from the existing actual measurable constructor, not necessary for the private nonexpansiveness argument and not a source correction.
p(y) is the actual proximal minimizer.	Constructed measurable p with genuine optimality equation and quantitative unique-minimum certificate.	source-implicit	Existence, measurability and identification are reused from the same parent rather than supplied as assumptions.
Bounds hold for all y,y',G,G'.	All inputs are arbitrary deterministic E vectors.	same	Gaussianity, integrability and expectation are irrelevant to these two pathwise assertions.
Lemma 4.2 additionally includes bias and centered exponential moments.	Only the two deterministic input-stability edges.	API-limitation	No full-lemma, score bias, concentration, Picard or paper completion is claimed.

Partial coverage of (4.4)-(4.5) for 0<eta<=1/2, inherited from the existing constructor, not a necessary mathematical threshold or a source repair. Finite-dimensional real inner-product spaces, including dimension zero, are a coordinate-free extension. No estimator bias, centered exponential moment, smoothed score, Picard accuracy, initialization or query-cost conclusion.

Encoder–denoiser: accepted · lean-strengthened-assumptions

Detected semantic differences

assumptions: Public theorem covers0<eta<=1/2, narrower than the source pointwise input estimates; this unchanged statement restriction is honestly documented as inherited from the measurable proximal constructor. It must not be counted as unrestricted source coverage. — Public hsmall, parent parameterized_contraction_point uniform1/2 iteration, lesson sources.scope and candidate_assumptions explicitly retain this limitation.
domains: Finite-dimensional real inner-product formulation, including dimension0, is an explicitly disclosed coordinate-free extension of the source Euclidean setting. — The typeclasses and zero-displacement branch preserve the mathematical argument; boundary test exercises Fin0 and eta=1/2.

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

Partial coverage of (4.4)-(4.5) for 0<eta≤1/2, inherited from the existing constructor, not a necessary mathematical threshold or a source repair. Finite-dimensional real inner-product spaces, including dimension zero, are a coordinate-free extension. No estimator bias, centered exponential moment, smoothed score, Picard accuracy, initialization or query-cost conclusion.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

LipschitzWith.of_dist_le_mul
LipschitzWith.dist_le_mul
real_inner_le_norm
real_inner_self_eq_norm_sq
DifferentiableAt.hasGradientAt
norm_smul
Real.sqrt_nonneg

Mathematical sources

SPHMC Lemma 4.2, equations (4.4)-(4.5) — Partial coverage of (4.4)-(4.5) for 0<eta<=1/2, inherited from the existing constructor, not a necessary mathematical threshold or a source repair. Finite-dimensional real inner-product spaces, including dimension zero, are a coordinate-free extension. No estimator bias, centered exponential moment, smoothed score, Picard accuracy, initialization or query-cost conclusion.

Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.

Actual proximal estimator: stability in both inputs

Complete source statement (Samplinglib restatement)

Pointwise input stability

Read the formalized proofs

Actual proximal estimator: stability in both inputs

Mathematical statement

Proof roadmap

All objects and hypotheses

Mathematical proof

1. Construct the same exact proximal oracle

2. Turn genuine Hessian bounds into gradient controls

3. Subtract optimality and pair with the displacement

4. Apply Cauchy-Schwarz and cancel only when permitted

5. Hold the noise fixed and compare centers

6. Hold the center fixed and compare noise inputs

Lean verification

Source assumptions versus formal assumptions

Detected semantic differences

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Mathematical sources

Which proof obligations and prerequisites are covered?