Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0

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

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

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

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

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

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

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

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'‖) := 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

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.