Expected work of the actual proximal-query program
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ProximalExpectedWork.approximate_proximal_expected_work · theorem · Teaching coverage
Mathematical statement
There exist measurable proximal points p and stopping indices N with measurable returned iterate x_N(y), where x_0(y)=y and x_(n+1)(y)=y−eta∇V(x_n(y)). They satisfy p(y)+eta∇V(p(y))=y and ‖x_N(y)−p(y)‖≤eps. The actual finite-fuel interpreter with N(y)+1 fuel returns (x_N(y),N(y)+1). Its real-valued query count is integrable under nu and has the following expectation bound.
Lean statement · approximate_proximal_expected_work
The exact adjacent declaration quantifies the input probability measure, genuine curvature bounds, moment hypothesis, constructed interpreter witnesses and integrable expected cost.
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_expected_work {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)
(ν : Measure E) [IsProbabilityMeasure ν]
(hmoment : Integrable (fun y => ‖gradient V y‖^2) ν) :
let T := fun y x : E => y - eta • gradient V x
let C := 2 + (1 + Real.log ((1-c)⁻¹)) / (-Real.log c)
∃ 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 ∧
‖(T y)^[N y] y - p y‖ ≤ eps ∧
ApproximateProximalExecution.proximalQuery (gradient V) eta eps y (N y+1) y =
some ((T y)^[N y] y, N y+1)) ∧
Integrable (fun y => (N y : ℝ) + 1) ν ∧
(∫ y, (N y : ℝ) + 1 ∂ν) ≤
C * (1 + Real.log (1 + Real.sqrt (∫ y, ‖gradient V y‖^2 ∂ν) / eps))Proof roadmap
- 1Use the real stopped program, not an assumed cost certificate
The existing execution theorem constructs p and N by contraction and the first successful residual test. Reuse these same witnesses, together with their measurable output, accuracy, and exact interpreter equation. In particular N+1 includes the final successful gradient evaluation.
- 2Establish integrability before taking expectations
C² regularity makes the gradient continuous and hence g measurable. The assumed integrable square gives g in L²; on a probability space this implies L¹. The nonnegative logarithm is bounded by g/eps, so it is integrable. The count is measurable, nonnegative, and dominated by an integrable multiple of one plus that logarithm.
- 3Apply Jensen on a closed positive domain
The variable 1+g/eps lies in [1,infinity). Restrict concavity and continuity of log to this closed convex half-line. Both the variable and its logarithm are integrable, so Mathlib's integral Jensen theorem applies without any improper-log convention.
- 4Compare the first and second moments
Nonnegative variance yields (E g)²≤E(g²). Since g and the square root are nonnegative, E g≤sqrt(E(g²)). This is the Cauchy–Schwarz step on a probability space, using Mathlib's variance identity rather than reproving a generic inequality.
- 5Integrate the pointwise work estimate
For 0<c<1, both −log c and 1−c are positive, and log((1−c)⁻¹) is nonnegative, so C_c≥0. Integrate the actual count bound, use linearity for the integrable terms, then combine Jensen and log monotonicity. No distributional identification or exchange of limiting integrals is needed.
Full assumptions and notation
All objects and hypotheses
- E is a finite-dimensional complete real inner-product space with its Borel sigma algebra. V:E→R is C², kappa≥1, and kappa⁻¹‖v‖²≤D²V(x)[v,v]≤‖v‖² for every x,v. The ContDiff assumption makes fderiv a genuine derivative.
- Fix 0<eta≤c<1 and eps>0. No eta≤1/2 restriction is introduced. The explicit constant depends only on c.
- nu is a probability measure on E and y↦‖gradient V y‖² is integrable. This moment hypothesis must later be established for the actual Picard center law; it is not silently assumed to follow from proximity in total variation.
Mathematical proof
1. Use the real stopped program, not an assumed cost certificate
The existing execution theorem constructs p and N by contraction and the first successful residual test. Reuse these same witnesses, together with their measurable output, accuracy, and exact interpreter equation. In particular N+1 includes the final successful gradient evaluation.
Corresponding Lean step
approximate_proximal_execution supplies hall. Its pointwise work conjunct becomes hbound; its actual execution conjunct is retained in the public conclusion.
2. Establish integrability before taking expectations
C² regularity makes the gradient continuous and hence g measurable. The assumed integrable square gives g in L²; on a probability space this implies L¹. The nonnegative logarithm is bounded by g/eps, so it is integrable. The count is measurable, nonnegative, and dominated by an integrable multiple of one plus that logarithm.
Corresponding Lean step
memLp_two_iff_integrable_sq and MemLp.integrable supply L¹. Real.log_le_sub_one_of_pos and Integrable.mono' prove log integrability; a second domination proves hcount.
3. Apply Jensen on a closed positive domain
The variable 1+g/eps lies in [1,infinity). Restrict concavity and continuity of log to this closed convex half-line. Both the variable and its logarithm are integrable, so Mathlib's integral Jensen theorem applies without any improper-log convention.
Corresponding Lean step
strictConcaveOn_log_Ioi is restricted to Set.Ici 1; ConcaveOn.le_map_integral checks the domain, closedness and both integrability obligations.
4. Compare the first and second moments
Nonnegative variance yields (E g)²≤E(g²). Since g and the square root are nonnegative, E g≤sqrt(E(g²)). This is the Cauchy–Schwarz step on a probability space, using Mathlib's variance identity rather than reproving a generic inequality.
Corresponding Lean step
variance_eq_sub is used only after MemLp g 2 is established; variance_nonneg and Real.sq_sqrt give hmean.
5. Integrate the pointwise work estimate
For 0<c<1, both −log c and 1−c are positive, and log((1−c)⁻¹) is nonnegative, so C_c≥0. Integrate the actual count bound, use linearity for the integrable terms, then combine Jensen and log monotonicity. No distributional identification or exchange of limiting integrals is needed.
Corresponding Lean step
integral_mono uses hcount and hdom; integral_const_mul and integral_add handle the integral; mul_le_mul_of_nonneg_left uses the checked sign hC.
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · approximate_proximal_expected_work
The public proof applies the existing actual-execution theorem. A private helper packages Mathlib Jensen, L²-to-L¹ and variance arguments; it has no separate leaf credit. No assumed accuracy or expected-cost oracle replaces the real program.
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_expected_work {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)
(ν : Measure E) [IsProbabilityMeasure ν]
(hmoment : Integrable (fun y => ‖gradient V y‖^2) ν) :
let T := fun y x : E => y - eta • gradient V x
let C := 2 + (1 + Real.log ((1-c)⁻¹)) / (-Real.log c)
∃ 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 ∧
‖(T y)^[N y] y - p y‖ ≤ eps ∧
ApproximateProximalExecution.proximalQuery (gradient V) eta eps y (N y+1) y =
some ((T y)^[N y] y, N y+1)) ∧
Integrable (fun y => (N y : ℝ) + 1) ν ∧
(∫ y, (N y : ℝ) + 1 ∂ν) ≤
C * (1 + Real.log (1 + Real.sqrt (∫ y, ‖gradient V y‖^2 ∂ν) / eps)) := by
dsimp only
obtain ⟨p, N, hp, hN, hout, hall⟩ :=
ApproximateProximalExecution.approximate_proximal_execution hκ hV hH heta hec hc heps
have hgcont : Continuous (gradient V) := by
unfold gradient
exact (InnerProductSpace.toDual ℝ E).symm.continuous.comp
(hV.continuous_fderiv (by norm_num))
have hg : Measurable (fun y => ‖gradient V y‖) := hgcont.norm.measurable
obtain ⟨hlog, hj⟩ := log_work_integral hg (fun y => norm_nonneg _) hmoment heps
let C := 2 + (1 + Real.log ((1-c)⁻¹)) / (-Real.log c)
have hC : 0 ≤ C := by
have hcp : 0 < c := heta.trans_le hec
have hd : 0 < 1-c := sub_pos.mpr hc
have ha : 0 < -Real.log c := neg_pos.mpr (Real.log_neg hcp hc)
have hb : 0 ≤ Real.log ((1-c)⁻¹) := Real.log_nonneg (by
have hm := mul_nonneg (inv_nonneg.mpr hd.le) hcp.le
have hi := inv_mul_cancel₀ hd.ne'
nlinarith)
dsimp [C]
positivity
have hbound (y) : (N y : ℝ)+1 ≤ C*(1+Real.log (1+‖gradient V y‖/eps)) :=
(hall y).2.2.2.2.2.1
have hdom : Integrable (fun y => C*(1+Real.log (1+‖gradient V y‖/eps))) ν :=
((integrable_const 1).add hlog).const_mul C
have hcount : Integrable (fun y => (N y : ℝ)+1) ν := by
apply hdom.mono' (by fun_prop)
filter_upwards [] with y
rw [Real.norm_of_nonneg (by positivity)]
exact hbound y
refine ⟨p, N, hp, hN, hout, fun y => ⟨(hall y).1, (hall y).2.2.2.2.1,
(hall y).2.2.2.2.2.2⟩, hcount, ?_⟩
calc
(∫ y, (N y : ℝ)+1 ∂ν) ≤ ∫ y, C*(1+Real.log (1+‖gradient V y‖/eps)) ∂ν :=
integral_mono hcount hdom hbound
_ = C*(1+∫ y, Real.log (1+‖gradient V y‖/eps) ∂ν) := by
rw [integral_const_mul, integral_add (integrable_const 1) hlog]
simp
_ ≤ _ := mul_le_mul_of_nonneg_left (add_le_add_right hj 1) hC
end
end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ProximalExpectedWorkSource assumptions versus formal assumptions
| Source | Actual Lean | Difference kind | Why it matters |
|---|---|---|---|
| Lemma D.4 concerns the actual Picard HMC center laws and first proves their numerical second-moment bound D.7. | An arbitrary probability measure nu is allowed, under the explicit premise Integrable(y↦‖∇V(y)‖²). | generalization | This isolates exactly the conditional Jensen consequence after D.7. The actual-law identification and numerical moment bound remain visible unsupported obligations, so this binding does not claim the full source lemma. |
| The source works on R^d with the normalized Hessian bounds and its stated algorithmic parameters. | Finite-dimensional complete real inner-product Borel space, genuine C² Hessian bounds, kappa≥1 and full 0<eta≤c<1, eps>0. | generalization | The coordinate-free domain contains the source Euclidean setting. C² prevents interpreting totalized fderiv as a derivative without regularity; the parameter range matches the parent D.3 execution theorem. |
| The proof invokes Lemma D.3's pointwise number of gradient evaluations and then Jensen's inequality. | The same measurable witnesses p,N returned by the actual finite-fuel interpreter are retained; N+1 is proved integrable before integral_mono and Jensen are used. | source-implicit | Measurability and integrability are logically required to take the displayed expectation. N+1 includes the successful residual-test query and is not a supplied cost assumption. |
| The paper writes a constant C and obtains the later bound C*L_q after inserting D.7 and parameter choices. | The conditional inequality uses the explicit admissible C_c=2+(1+log((1-c)^-1))/(-log c) inherited from the formal D.3 bound. | source-implicit | This makes the c-dependence explicit without claiming the later L_q estimate or D.8. The formula was derived in Samplinglib and is not printed verbatim in the paper. |
Conditional expected work for one actual stopped proximal query. No proof that the realized Picard center law satisfies D.7, no uniform C*kappa*d*L_q^18 moment bound, no 2J-per-phase/number-of-phases aggregation, no D.8, approximate-kernel stability, sampling accuracy or full-paper result. Total variation is not used to transfer unbounded cost.
Encoder–denoiser: source-reviewed · equivalent-after-elaboration
Detected semantic differences
- conclusion: Lean constructs measurable stopped-program witnesses and proves count integrability, details implicit in the paper's use of a random Algorithm D.2 cost. — Independent source review classification: explicit-elaboration; nonblocking.
- scopes: Lean states the conditional Jensen estimate for an arbitrary probability center law with a finite square-gradient moment; D.7 is intentionally left as a later instantiation obligation. — Independent source review classification: explicit-elaboration; nonblocking.
- domains: The Euclidean source domain is generalized coordinate-free to finite-dimensional complete real inner-product Borel spaces. — Independent source review classification: explicit-elaboration; nonblocking.
- constant_dependencies: Lean exposes one admissible formula for the D.3 constant C_c, whose dependence only on c is consistent with the source's C_c notation. — Independent source review classification: explicit-elaboration; nonblocking.
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
- The Jensen step in D.4 only, conditional on a finite input gradient second moment. This does not prove the Picard input moment bound (D.7), approximate-query stability, the phase count, total cost (D.8), or either complete paper. Publication admission is tracked separately from compilation.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
Mathlib API called (external library)
- MeasureTheory.memLp_two_iff_integrable_sq
- MeasureTheory.MemLp.integrable
- MeasureTheory.Integrable.mono'
- Real.log_le_sub_one_of_pos
- strictConcaveOn_log_Ioi
- ConcaveOn.le_map_integral
- ProbabilityTheory.variance_eq_sub
- ProbabilityTheory.variance_nonneg
- Real.sq_sqrt
- MeasureTheory.integral_mono
Mathematical sources
- Chen–Chewi–Lu–Zhang, SPHMC Lemma D.4 proof after (D.7) — Attributed expansion of the expectation/Jensen step, not the full lemma.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.