Measurable stopped proximal execution with certified pointwise work
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ApproximateProximalExecution.approximate_proximal_execution · theorem · Teaching coverage
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)].
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.
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)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).
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).
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.
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.
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.
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.
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.
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.
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 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.ApproximateProximalExecutionSource assumptions versus formal assumptions
| Source | Actual Lean | Difference kind | Why it matters |
|---|---|---|---|
| Finite-dimensional Euclidean potential and curvature bounds. | Finite-dimensional complete real inner-product Borel space, C² V, genuine Hessian bounds and kappa≥1. | generalization | Coordinate-free representation includes the source Euclidean setting; C² ensures totalized fderiv denotes the genuine Hessian. |
| 0<eta≤c₀<1 and positive target error. | 0<eta≤c<1 and eps>0, without eta≤1/2. | same | The contraction proof covers the full stated parameter range. |
| Return the current tested iterate; count gradient evaluations. | Noncomputable exact-real finite-fuel interpreter returns (x_N,N+1). | source-implicit | Every tested residual spends one query, including the successful test. This does not model floating-point rounding or export machine code. |
| C_c₀ depends only on c₀; proximity to the proximal point. | An explicit finite C_c and quadratic growth at the unique proximal minimum; measurable p, N and stopped output. | source-implicit | These are derived certificates and measurability details, not extra premises. No integration or expected-cost claim is made. |
Pointwise D.2/D.3 execution only. Expected work along the realized Picard run (D.4), D.1 stability, sampling accuracy and the main paper remain separate. The interpreter records point/count but not a query-list trace; its successful fuel is N+1, with no arbitrary-excess-fuel theorem.
Encoder–denoiser: source-reviewed · equivalent-after-elaboration
Detected semantic differences
- domains: Compared with the primary article, the pinned expanded contract uses coordinate-free finite-dimensional Borel spaces. — The packet explicitly discloses this change; the reconstructed typeclasses match that disclosure and include Euclidean spaces.
- conclusion: Compared with D.3 alone, the pinned expanded contract adds measurability, quantitative uniqueness and exact interpreter semantics. — These are explicitly attributed to Samplinglib and are established by the supplied module. They are not additional changes introduced by the blind reconstruction.
- constant_dependencies: The explicit coefficient is a derived admissible choice, not a constant printed in the cited lemma. — The candidate formula and proof disclose its provenance; the module's count_bound supplies the matching derivation.
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
- 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
AutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticRegularization.strongConvexOn_and_lipschitzWith_gradient_add_quadraticAutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticRegularizationFirstOrder.curvature_gradient_and_smoothnessAutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexFirstOrder.firstOrder_lower_bound_of_strongConvexOn
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.