ApproximateProximalExecution: 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.

A gradient-query interpreter that counts the successful test
Measurable stopped proximal execution with certified pointwise work

Samplinglib mathematical lesson

A gradient-query interpreter that counts the successful test

AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ApproximateProximalExecution.proximalQuery · def · Teaching coverage

Read this first

Mathematical statement

With no fuel return none. Otherwise evaluate g at x, form z=y−eta g(x), and test the residual. Success returns the current x and count one. Failure recurses at z with one less fuel and adds one to a successful returned count; unsuccessful recursion returns none.

\[Q_0(x)=\mathrm{none},\qquad Q_{m+1}(x)=\begin{cases}\mathrm{some}(x,1),&\|y-\eta g(x)-x\|\le(1-\eta)\varepsilon,\\\mathrm{map}((u,k)\mapsto(u,k+1),Q_m(y-\eta g(x))),&\text{otherwise}.\end{cases}\]

Lean statement · proximalQuery

The adjacent disclosure extracts the exact oracle, real parameters, natural fuel, and Option-valued return type from Lean.

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)

noncomputable def proximalQuery (g : E → E) (eta eps : ℝ) (y : E) :
    ℕ → E → Option (E × ℕ)
  | 0, _ => none
  | n+1, x => by
    classical
    let z := y-eta • g x
    exact if ‖z-x‖ ≤ (1-eta)*eps then some (x,1)
      else (proximalQuery g eta eps y n z).map (fun r => (r.1,r.2+1))

Exact module and namespace context

Proof roadmap

1Spend one query before testing
Even an immediately successful residual test needs the gradient at the current point. The let-bound z represents that single oracle evaluation. Mathematical arithmetic and comparison are exact; this is not a numerical-roundoff model.
2Return the tested point, not the next point
The certificate in the companion theorem controls the error at x through the residual between x and z. Therefore the successful branch returns x. Each unsuccessful level contributes exactly one additional query to the recursively returned count.

Full assumptions and notation

All objects and hypotheses

E is a real normed vector space. g:E→E is an arbitrary oracle, eta and eps are real parameters, y is the fixed center, x is the current point, and fuel is a natural number. No regularity or positivity is required just to define the interpreter.

Construction and meaning

1. Spend one query before testing

Even an immediately successful residual test needs the gradient at the current point. The let-bound z represents that single oracle evaluation. Mathematical arithmetic and comparison are exact; this is not a numerical-roundoff model.

\[z=y-\eta g(x),\qquad r=\|z-x\|.\]

Corresponding Lean step

The positive-fuel branch binds z before the if; success is some (x,1).

2. Return the tested point, not the next point

The certificate in the companion theorem controls the error at x through the residual between x and z. Therefore the successful branch returns x. Each unsuccessful level contributes exactly one additional query to the recursively returned count.

\[\mathrm{returned\ point}=x,\qquad\mathrm{count}=1+\mathrm{recursive\ count}.\]

Corresponding Lean step

Option.map preserves failure and increments only the count in a successful pair; run_first_stop proves the recurrence's execution equation.

Lean verification

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

Lean construction · proximalQuery

This is a recursive definition, not an independently proved accuracy theorem. Its execution is certified by approximate_proximal_execution.

Download module (.lean)

noncomputable def proximalQuery (g : E → E) (eta eps : ℝ) (y : E) :
    ℕ → E → Option (E × ℕ)
  | 0, _ => none
  | n+1, x => by
    classical
    let z := y-eta • g x
    exact if ‖z-x‖ ≤ (1-eta)*eps then some (x,1)
      else (proximalQuery g eta eps y n z).map (fun r => (r.1,r.2+1))

Exact module and namespace context

Scope and omitted-condition boundaries

Exact-real noncomputable finite-fuel semantics, not floating-point software. This definition alone proves neither termination nor accuracy. It records output and count, not a query-list trace.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Option.map

Mathematical sources

Chen–Chewi–Lu–Zhang, SPHMC Algorithm D.2 — Attributed paraphrase; Samplinglib's finite-fuel representation is explicit implementation structure.

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

Samplinglib mathematical lesson

Measurable stopped proximal execution with certified pointwise work

AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ApproximateProximalExecution.approximate_proximal_execution · theorem · Teaching coverage

Read this first

Mathematical statement

There exist measurable maps p:E→E and N:E→N. For each y, p(y) is the unique minimizer of F_y(x)=V(x)+‖x−y‖²/(2eta). Starting at y and iterating T_y(x)=y−eta∇V(x), N(y) is the first residual test success. The measurable returned point x_N is eps-close to p(y); the exact interpreter succeeds with fuel N(y)+1, returning that point and count N(y)+1, bounded by C_c[1+log(1+‖∇V(y)‖/eps)].

\[\begin{gathered}x_0=y,\quad x_{n+1}=T_y(x_n),\quad N=\min\{n:\|x_{n+1}-x_n\|\le(1-\eta)\varepsilon\},\\\|x_N-p(y)\|\le\varepsilon,\quad N+1\le C_c[1+\log(1+\|\nabla V(y)\|/\varepsilon)],\\C_c=2+\frac{1+\log((1-c)^{-1})}{-\log c}.\end{gathered}\]

Lean statement · approximate_proximal_execution

Exact scoped typeclasses, every quantifier, genuine Hessian bounds and all conjuncts are extracted into the adjacent closed disclosure.

Download module (.lean)

theorem approximate_proximal_execution {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 c eps : ℝ} (heta : 0 < eta) (hec : eta ≤ c) (hc : c < 1) (heps : 0 < eps) :
    let T := fun y x : E => y-eta • gradient V x
    let F := fun y x => V x+eta⁻¹/2*‖x-y‖^2
    ∃ p : E → E, ∃ N : E → ℕ,
      Measurable p ∧ Measurable N ∧ Measurable (fun y => (T y)^[N y] y) ∧
      ∀ y, (p y+eta • gradient V (p 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)) ∧
        ‖(T y)^[N y+1] y-(T y)^[N y] y‖ ≤ (1-eta)*eps ∧
        (∀ j < N y, ¬ ‖(T y)^[j+1] y-(T y)^[j] y‖ ≤ (1-eta)*eps) ∧
        ‖(T y)^[N y] y-p y‖ ≤ eps ∧
        (N y : ℝ)+1 ≤ (2+(1+Real.log ((1-c)⁻¹))/(-Real.log c)) *
          (1+Real.log (1+‖gradient V y‖/eps)) ∧
        proximalQuery (gradient V) eta eps y (N y+1) y = some ((T y)^[N y] y,N y+1)

Exact module and namespace context

Proof roadmap

1Curvature gives a strict contraction
The canonical quadratic-regularization lemma at zero regularization gives a 1-Lipschitz gradient and strong convexity of V. Subtracting two images under T_y cancels the center, so multiplication by eta gives a strict contraction. Completeness then supplies its unique fixed point p(y).
2Identify a genuine unique proximal minimum
The canonical first-order regularization formula shows that the fixed point has zero gradient for F_y. Its strong-convexity modulus is kappa inverse plus eta inverse. Applying the first-order lower bound at that point gives quantitative quadratic growth. Its strictly positive coefficient forces any other minimizer to coincide with p(y).
3Produce a finite stopping certificate
Successive residuals decay geometrically. Put z=‖∇V(y)‖ and t=(1−c)eps, both with t strictly positive. Taking the natural ceiling B below gives c^B≤1/(1+z/t), hence z c^B≤t. Since eta≤c and eta<1, the actual residual at B is no larger than t and therefore passes the test. This establishes existence before selecting a first index.
4Explain the measurability that a sampler needs
Every iterate is measurable as a function of y by induction and continuity of the gradient. Their pointwise limit is p(y), hence measurable. Each residual-test set is Borel. The least successful index is measurable, and selecting the N(y)-th member of this countable measurable family yields a measurable returned point. No integration or exchange of integrals is used.
5Convert the residual to actual distance
The contraction posterior-error estimate bounds the current iterate's distance to the fixed point by its residual divided by 1−eta. The denominator is strictly positive. At the selected first hit the test is exactly strong enough to bound this quotient by eps.
6Bound the number of real oracle queries
The ceiling estimate first gives N+1≤2+log(1+z/((1−c)eps))/(-log c). For R=z/eps, use 1+R/(1−c)≤(1+R)/(1−c), then log monotonicity. The displayed C_c dominates the resulting affine expression in log(1+R). It is an explicit Samplinglib choice, not a constant printed in the source; it depends only on c. When the initial gradient vanishes, one query is still required.
7Tie the proof to the actual interpreter
All tests before N fail and the test at N succeeds. Induction over these failed tests unfolds one interpreter step at a time. The final step returns the current point with one query; unwinding increments the count to N+1. This is a pointwise evaluation theorem, not a theorem about expectations for randomly generated centers.

Full assumptions and notation

All objects and hypotheses

E is a finite-dimensional complete real inner-product space with its Borel measurable structure. This includes Euclidean space and dimension zero.
V:E→R is C², kappa≥1, and for every x,v its genuine second derivative satisfies kappa⁻¹‖v‖²≤D²V(x)[v,v]≤‖v‖². ContDiff makes the displayed fderiv a genuine derivative, not merely a totalized expression.
Fix 0<eta≤c<1 and eps>0. The constant c is uniform in the center y. No restriction eta≤1/2 is imposed. There is no assumed approximate proximal oracle and no assumed measurability of the output.

Mathematical proof

1. Curvature gives a strict contraction

The canonical quadratic-regularization lemma at zero regularization gives a 1-Lipschitz gradient and strong convexity of V. Subtracting two images under T_y cancels the center, so multiplication by eta gives a strict contraction. Completeness then supplies its unique fixed point p(y).

\[\|T_y(x)-T_y(z)\|\le\eta\|x-z\|,\qquad p(y)+\eta\nabla V(p(y))=y.\]

Corresponding Lean step

QuadraticRegularization supplies hg; stopped_contraction constructs ContractingWith and its fixedPoint.

2. Identify a genuine unique proximal minimum

The canonical first-order regularization formula shows that the fixed point has zero gradient for F_y. Its strong-convexity modulus is kappa inverse plus eta inverse. Applying the first-order lower bound at that point gives quantitative quadratic growth. Its strictly positive coefficient forces any other minimizer to coincide with p(y).

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

Corresponding Lean step

curvature_gradient_and_smoothness proves the gradient identity; firstOrder_lower_bound_of_strongConvexOn proves growth, then positivity proves uniqueness.

3. Produce a finite stopping certificate

Successive residuals decay geometrically. Put z=‖∇V(y)‖ and t=(1−c)eps, both with t strictly positive. Taking the natural ceiling B below gives c^B≤1/(1+z/t), hence z c^B≤t. Since eta≤c and eta<1, the actual residual at B is no larger than t and therefore passes the test. This establishes existence before selecting a first index.

\[\begin{gathered}\|x_{n+1}-x_n\|\le\eta^{n+1}\|\nabla V(y)\|,\\ B=\left\lceil\frac{\log(1+z/t)}{-\log c}\right\rceil,\quad zc^B\le t\le(1-\eta)\varepsilon,\quad N\le B.\end{gathered}\]

Corresponding Lean step

dist_iterate_succ_le_geometric and geometric_certificate prove hcert; Nat.find_spec/min/min' give success, first-hit minimality and the bound.

4. Explain the measurability that a sampler needs

Every iterate is measurable as a function of y by induction and continuity of the gradient. Their pointwise limit is p(y), hence measurable. Each residual-test set is Borel. The least successful index is measurable, and selecting the N(y)-th member of this countable measurable family yields a measurable returned point. No integration or exchange of integrals is used.

\[\{N=n\}=A_n\cap\bigcap_{j<n}A_j^c,\qquad A_n=\{y:\|x_{n+1}(y)-x_n(y)\|\le(1-\eta)\varepsilon\}.\]

Corresponding Lean step

measurable_of_tendsto_metrizable, measurable_find and Measurable.find discharge limit, index and selected-output measurability.

5. Convert the residual to actual distance

The contraction posterior-error estimate bounds the current iterate's distance to the fixed point by its residual divided by 1−eta. The denominator is strictly positive. At the selected first hit the test is exactly strong enough to bound this quotient by eps.

\[\|x_N-p(y)\|\le\frac{\|x_{N+1}-x_N\|}{1-\eta}\le\varepsilon.\]

Corresponding Lean step

ContractingWith.aposteriori_dist_iterate_fixedPoint_le followed by div_le_iff₀; the bound concerns x_N, not x_(N+1).

6. Bound the number of real oracle queries

The ceiling estimate first gives N+1≤2+log(1+z/((1−c)eps))/(-log c). For R=z/eps, use 1+R/(1−c)≤(1+R)/(1−c), then log monotonicity. The displayed C_c dominates the resulting affine expression in log(1+R). It is an explicit Samplinglib choice, not a constant printed in the source; it depends only on c. When the initial gradient vanishes, one query is still required.

\[N+1\le2+\frac{\log(1+R)+\log((1-c)^{-1})}{-\log c}\le C_c[1+\log(1+R)].\]

Corresponding Lean step

count_bound uses Nat.ceil_lt_add_one and Real.log_div; positivity uses 0<c<1 and R≥0.

7. Tie the proof to the actual interpreter

All tests before N fail and the test at N succeeds. Induction over these failed tests unfolds one interpreter step at a time. The final step returns the current point with one query; unwinding increments the count to N+1. This is a pointwise evaluation theorem, not a theorem about expectations for randomly generated centers.

\[Q_{N+1}(y)=\mathrm{some}(x_N,N+1).\]

Corresponding Lean step

run_first_stop proves the recurrence equation; focused tests exercise returned point, count, insufficient fuel and eta=3/4.

Lean verification

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

Lean proof · approximate_proximal_execution

The public proof reuses shared curvature/first-order lemmas; private helpers prove the logarithmic certificate, measurable stopped contraction, count bound and execution induction. Private helpers have no separate mathematical completion credit.

Download module (.lean)

theorem approximate_proximal_execution {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 c eps : ℝ} (heta : 0 < eta) (hec : eta ≤ c) (hc : c < 1) (heps : 0 < eps) :
    let T := fun y x : E => y-eta • gradient V x
    let F := fun y x => V x+eta⁻¹/2*‖x-y‖^2
    ∃ p : E → E, ∃ N : E → ℕ,
      Measurable p ∧ Measurable N ∧ Measurable (fun y => (T y)^[N y] y) ∧
      ∀ y, (p y+eta • gradient V (p 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)) ∧
        ‖(T y)^[N y+1] y-(T y)^[N y] y‖ ≤ (1-eta)*eps ∧
        (∀ j < N y, ¬ ‖(T y)^[j+1] y-(T y)^[j] y‖ ≤ (1-eta)*eps) ∧
        ‖(T y)^[N y] y-p y‖ ≤ eps ∧
        (N y : ℝ)+1 ≤ (2+(1+Real.log ((1-c)⁻¹))/(-Real.log c)) *
          (1+Real.log (1+‖gradient V y‖/eps)) ∧
        proximalQuery (gradient V) eta eps y (N y+1) y = some ((T y)^[N y] y,N y+1) := by
  have hκpos : 0 < (κ : ℝ) := lt_of_lt_of_le zero_lt_one (by exact_mod_cast hκ)
  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 hr := TechnicalLemmas.Analysis.QuadraticRegularization.strongConvexOn_and_lipschitzWith_gradient_add_quadratic
    (r := 0) hV hH' (0 : E)
  have hg : LipschitzWith 1 (gradient V) := by simpa using hr.2
  have hvconv : ConvexOn ℝ Set.univ V := by
    have hs : StrongConvexOn Set.univ ((κ : ℝ)⁻¹) V := by simpa using hr.1
    exact hs.convexOn (fun r => by positivity)
  obtain ⟨p,N,hp,hN,ho,hall⟩ := stopped_contraction hg heta hec hc heps
  refine ⟨p,N,hp,hN,ho,fun y => ?_⟩
  obtain ⟨heq,hs,hbefore,herr,hcap,hrun⟩ := hall y
  refine ⟨heq,?_,hs,hbefore,herr,count_bound (heta.trans_le hec) hc
    (norm_nonneg _) heps hcap,hrun⟩
  let F := fun x => V x+eta⁻¹/2*‖x-y‖^2
  have hdiff := hV.differentiable (by norm_num)
  have hdata := TechnicalLemmas.Analysis.QuadraticRegularizationFirstOrder.curvature_gradient_and_smoothness
    hdiff hvconv (δ := Real.toNNReal eta⁻¹) hg y
  have hgrad (x : E) : gradient F x = gradient V x+eta⁻¹ • (x-y) := by
    simpa only [Real.coe_toNNReal _ (inv_nonneg.mpr heta.le)] using hdata.2.2.1 x
  have hFd : Differentiable ℝ F := by
    simpa only [Real.coe_toNNReal _ (inv_nonneg.mpr heta.le)] using hdata.1
  have hz : gradient F (p y)=0 := by
    rw [hgrad]
    have hsub : p y-y=-(eta • gradient V (p y)) := by
      calc
        p y-y = p y-(p y+eta • gradient V (p y)) :=
          congrArg (fun t => p y-t) heq.symm
        _ = _ := by abel
    rw [hsub,smul_neg,smul_smul,inv_mul_cancel₀ heta.ne',one_smul,add_neg_cancel]
  have hsc : StrongConvexOn Set.univ ((κ : ℝ)⁻¹+eta⁻¹) F := by
    have hh := TechnicalLemmas.Analysis.QuadraticRegularization.strongConvexOn_and_lipschitzWith_gradient_add_quadratic
      (r := Real.toNNReal eta⁻¹) hV hH' y
    simpa only [NNReal.coe_add, NNReal.coe_inv, Real.coe_toNNReal _ (inv_nonneg.mpr heta.le)] using hh.1
  intro z
  have hb := TechnicalLemmas.Analysis.StrongConvexFirstOrder.firstOrder_lower_bound_of_strongConvexOn
    hsc (fun x _ => (hFd x).hasGradientAt) (x := p y) (y := z) (Set.mem_univ _) (Set.mem_univ _)
  rw [hz,inner_zero_left,add_zero] at hb
  refine ⟨hb,⟨fun hle => ?_,fun he => by rw [he]⟩⟩
  have ha : 0 < ((κ : ℝ)⁻¹+eta⁻¹)/2 := by positivity
  have hn : ‖z-p y‖^2 ≤ 0 := by
    change F z ≤ F (p y) at hle
    have hnonpos : (((κ : ℝ)⁻¹+eta⁻¹)/2)*‖z-p y‖^2 ≤ 0 := by linarith
    exact le_of_not_gt (fun hn => (not_lt_of_ge hnonpos) (mul_pos ha hn))
  exact sub_eq_zero.mp (norm_eq_zero.mp (sq_eq_zero_iff.mp (le_antisymm hn (sq_nonneg _))))

end

end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ApproximateProximalExecution

Exact module and namespace context

Scope and omitted-condition boundaries

Algorithm D.2/Lemma D.3 only. No expected cost along a sampler, Picard moment bound, D.1 stability bound, sampling convergence or full SPHMC result is proved here. Independent encoder-denoiser publication admission is pending.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

ContractingWith.fixedPoint
ContractingWith.aposteriori_dist_iterate_fixedPoint_le
LipschitzWith.dist_iterate_succ_le_geometric
measurable_of_tendsto_metrizable
measurable_find
Measurable.find
Nat.find_spec
Nat.ceil_lt_add_one
Real.log_div

Mathematical sources

Fan Chen, Sinho Chewi, Jianfeng Lu and Matthew S. Zhang, SPHMC D.2–D.3 — Faithful attributed restatement with Samplinglib-derived measurability, quantitative unique minimum, exact interpreter semantics and explicit admissible constant.

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