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.

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