Samplinglib
Lean gate not recorded for this source state main · 0e31a3cda412

ProximalEstimatorLipschitz: mathematical reading route

Read the statements and derivations in source order. Every result has its own optional Lean statement and proof. Source assumptions, library reuse and unproved boundaries are kept explicit.

  1. Actual proximal estimator: stability in both inputs
ASTIS mathematical exposition

Actual proximal estimator: stability in both inputs

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

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'\|.\]

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 substantive new resolvent step, 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

private 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 private 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

hbound,hzero,hpos; LipschitzWith.of_dist_le_mul; 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 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.

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

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.

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_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 := 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

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.

Source and reuse

ASTIS 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.

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