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