From a genuine Hessian lower bound to strong convexity
AutoSamplingTheory.TechnicalLemmas.Analysis.HessianStrongConvexity.strongConvexOn_univ_of_fderiv2_lower · theorem · Teaching coverage
Mathematical statement
Let E be a real normed space, let V:E→R be twice continuously Fréchet differentiable everywhere, and let α be any real number. Suppose D²V(x)[v,v]≥α‖v‖² for every x,v∈E. Then V is α-strongly convex on the whole space in the chord convention below. No finite dimension, completeness, inner product, positive α, upper Hessian bound, measure or normalizer is an additional hypothesis.
Lean statement · strongConvexOn_univ_of_fderiv2_lower
The public theorem quantifies over any real normed E, V:E→ℝ and α:ℝ. Its two hypotheses are ContDiff ℝ 2 V and the everywhere, every-direction nested-fderiv diagonal lower bound. The conclusion is Mathlib StrongConvexOn Set.univ α V. There is no assumed gradient or Hessian field with a separate unproved identification.
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 strongConvexOn_univ_of_fderiv2_lower
{E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
{V : E → ℝ} {α : ℝ}
(hV : ContDiff ℝ 2 V)
(hH : ∀ x v : E, α * ‖v‖ ^ 2 ≤ (fderiv ℝ (fderiv ℝ V) x v) v) :
StrongConvexOn (Set.univ : Set E) α VProof roadmap
- 1Restrict to a line and compensate its curvature
Fix x,y∈E and set v=y−x and c=α‖v‖². Restrict V to the line ℓ(t)=x+tv, then subtract the scalar quadratic ct²/2. The norm of v is a fixed number: the proof never differentiates the norm on E, which is why no inner product or smooth norm is needed.
- 2Calculate two genuine scalar derivatives
The chain rule differentiates V along the constant direction v. Applying the chain rule to DV and then evaluating at the fixed vector v gives the second derivative. The assumed diagonal Hessian inequality therefore makes the compensated second derivative nonnegative.
- 3Use one-dimensional convexity
A scalar function with the displayed genuine first and second derivatives and nonnegative second derivative is convex. Continuity of q follows from its first derivative witness. Applying its chord inequality at 0 and 1 with weights a,b≥0 and a+b=1 controls q(b).
- 4Recover the exact strong-convexity constant
Since x+b(y−x)=ax+by and ‖y−x‖=‖x−y‖, rearrange the scalar chord inequality and use b(1−b)=ab. This is algebra, not multiplication of an inequality by α, so it is valid even when α is zero or negative.
Full assumptions and notation
All objects and hypotheses
- ContDiff ℝ 2 V is a genuine C² witness. D²V(x)[v,v] means (fderiv ℝ (fderiv ℝ V) x v) v; the regularity hypothesis ensures these totalized operators represent actual derivatives.
- The Hessian lower bound holds at every point and in every direction, not almost everywhere or only along algorithmic iterates.
- The papers use Euclidean spaces and 0<α≤β with an upper Hessian bound βI. This supporting implication only needs their lower bound, and remains valid on arbitrary real normed spaces for any real α.
- The domain is the whole vector space, so every affine line used in the proof is admissible. No boundary extension or differentiability-within-set convention is hidden.
Mathematical proof
1. Restrict to a line and compensate its curvature
Fix x,y∈E and set v=y−x and c=α‖v‖². Restrict V to the line ℓ(t)=x+tv, then subtract the scalar quadratic ct²/2. The norm of v is a fixed number: the proof never differentiates the norm on E, which is why no inner product or smooth norm is needed.
Corresponding Lean step
The proof defines v, c and q locally after opening the StrongConvexOn chord goal. hV.differentiable gives differentiability of V; hV.fderiv_right at order one gives differentiability of its actual first derivative. hline is the derivative witness for the affine line.
2. Calculate two genuine scalar derivatives
The chain rule differentiates V along the constant direction v. Applying the chain rule to DV and then evaluating at the fixed vector v gives the second derivative. The assumed diagonal Hessian inequality therefore makes the compensated second derivative nonnegative.
Corresponding Lean step
hq' and hq'' are HasDerivAt proofs, obtained from HasFDerivAt.comp_hasDerivAt, HasDerivAt.clm_apply and the scalar polynomial rules. Explicit reflexivity conversions reconcile definitionally equal scalar instances; they add no mathematical premise. hH supplies the final nonnegativity.
3. Use one-dimensional convexity
A scalar function with the displayed genuine first and second derivatives and nonnegative second derivative is convex. Continuity of q follows from its first derivative witness. Applying its chord inequality at 0 and 1 with weights a,b≥0 and a+b=1 controls q(b).
Corresponding Lean step
convexOn_of_hasDerivWithinAt2_nonneg is applied on Set.univ. Each whole-line HasDerivAt witness supplies the required HasDerivWithinAt witness. hconv.2 then yields hchord at the endpoints 0 and 1.
4. Recover the exact strong-convexity constant
Since x+b(y−x)=ax+by and ‖y−x‖=‖x−y‖, rearrange the scalar chord inequality and use b(1−b)=ab. This is algebra, not multiplication of an inequality by α, so it is valid even when α is zero or negative.
Corresponding Lean step
hxy and hend identify the line points with the desired chord and endpoint; norm_sub_rev identifies the two displacement norms. Substituting a=1−b and polynomial arithmetic gives the defining StrongConvexOn inequality with exactly α/2.
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · strongConvexOn_univ_of_fderiv2_lower
This declaration is a new mathematical adapter built from Mathlib calculus and one-dimensional convexity. It calls no ASTIS production theorem. In the focused tests, its positive-α finite-dimensional Borel inner-product specialization feeds the existing ASTIS StrongConvexGibbsIntegrability theorem. The tests derive Integrable and a strictly positive canonical-volume Gibbs integral, then an actual IsProbabilityMeasure for volume.tilted(-V), which supplies the probability input of the existing quadratic_tilt_tilt RGO consumer. The tests assume neither StrongConvexOn nor integrability. Separate tests cover α=0 and zero dimension.
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 strongConvexOn_univ_of_fderiv2_lower
{E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
{V : E → ℝ} {α : ℝ}
(hV : ContDiff ℝ 2 V)
(hH : ∀ x v : E, α * ‖v‖ ^ 2 ≤ (fderiv ℝ (fderiv ℝ V) x v) v) :
StrongConvexOn (Set.univ : Set E) α V := by
have hVd : Differentiable ℝ V := hV.differentiable (by norm_num)
have hVdd : Differentiable ℝ (fderiv ℝ V) :=
(hV.fderiv_right (m := 1) (by norm_num)).differentiable_one
refine ⟨convex_univ, ?_⟩
intro x _ y _ a b ha hb hab
let v : E := y - x
let c : ℝ := α * ‖v‖ ^ 2
let q : ℝ → ℝ := fun t => V (x + t • v) - c / 2 * t ^ 2
let q' : ℝ → ℝ := fun t => fderiv ℝ V (x + t • v) v - c * t
let q'' : ℝ → ℝ := fun t =>
(fderiv ℝ (fderiv ℝ V) (x + t • v) v) v - c
have hline (t : ℝ) : HasDerivAt (fun s : ℝ => x + s • v) v t := by
simpa using ((hasDerivAt_id t).smul_const v).const_add x
have hq' (t : ℝ) : HasDerivAt q (q' t) t := by
have hquadratic : HasDerivAt (fun s : ℝ => c / 2 * s ^ 2) (c * t) t := by
convert ((hasDerivAt_id t).pow 2).const_mul (c / 2) using 1 <;>
first | rfl | (norm_num [id_eq]; ring)
convert ((hVd _).hasFDerivAt.comp_hasDerivAt t (hline t)).sub hquadratic
using 1 <;> rfl
have hq'' (t : ℝ) : HasDerivAt q' (q'' t) t := by
have hfirst := ((hVdd _).hasFDerivAt.comp_hasDerivAt t (hline t)).clm_apply
(hasDerivAt_const t v)
convert hfirst.sub ((hasDerivAt_id t).const_mul c) using 1 <;>
first | rfl | simp [q'', ContinuousLinearMap.map_zero]
have hconv : ConvexOn ℝ Set.univ q :=
convexOn_of_hasDerivWithinAt2_nonneg convex_univ
(fun t _ => (hq' t).continuousAt.continuousWithinAt)
(fun t _ => (hq' t).hasDerivWithinAt)
(fun t _ => (hq'' t).hasDerivWithinAt)
(fun t _ => sub_nonneg.mpr (hH (x + t • v) v))
have hchord := hconv.2 (x := 0) (Set.mem_univ _) (y := 1) (Set.mem_univ _)
ha hb hab
have hxy : x + b • v = a • x + b • y := by
dsimp only [v]
rw [show a = 1 - b by linarith]
module
have hend : x + v = y := by simp [v]
simp only [q, smul_eq_mul, mul_zero, mul_one, zero_add, zero_smul, add_zero,
one_pow, one_smul] at hchord
norm_num only [zero_pow, mul_zero, sub_zero] at hchord
rw [hxy, hend] at hchord
have hnorm : ‖v‖ ^ 2 = ‖x - y‖ ^ 2 := by
dsimp only [v]
rw [norm_sub_rev]
change V (a • x + b • y) ≤ a * V x + b * V y - a * b * (α / 2 * ‖x - y‖ ^ 2)
dsimp only [c] at hchord
rw [hnorm] at hchord
rw [show a = 1 - b by linarith] at hchord ⊢
nlinarith
end AutoSamplingTheory.TechnicalLemmas.Analysis.HessianStrongConvexitySource assumptions versus formal assumptions
| Source | Actual Lean | Difference kind | Why it matters |
|---|---|---|---|
| V is everywhere C² | ContDiff ℝ 2 V | same | This supplies actual first and second Fréchet derivatives, rather than relying on totalized derivative notation alone. |
| αI≼∇²V(x) pointwise | ∀ x v, α*‖v‖² ≤ (fderiv ℝ (fderiv ℝ V) x v) v | same | For a C² Euclidean potential this is the defining quadratic-form meaning of the Hessian lower bound. No separate field is assumed to be the Hessian. |
| Euclidean finite-dimensional state space | Any real normed space, including zero dimension | generalization | The proof differentiates only a scalar line and its scalar quadratic compensation, not the squared norm on the ambient space. No inner product, completeness or finite dimension is used. |
| 0<α≤β and the additional upper Hessian bound βI | Arbitrary α:ℝ; no β or upper Hessian bound | generalization | Only the lower bound controls the compensated second derivative. The concluding algebra works for any α. This does not remove positivity or smoothness conditions from either source sampling theorem. |
| Strong convexity in the C² Hessian convention | StrongConvexOn Set.univ α V, with chord correction αab‖x−y‖²/2 | source-implicit | The selected analytic expansion proves the conversion to the exact chord normalization. It does not assume StrongConvexOn or change α to a weaker constant. |
One analytic prerequisite shared by both papers. No upper-Hessian theorem, entire Gibbs/RGO initialization, invariance, discrepancy or query-cost guarantee is proved by this declaration.
Encoder–denoiser: accepted · equivalent-after-elaboration
Detected semantic differences
- domains: The analytic theorem is explicitly generalized from the source's Euclidean space to arbitrary real normed spaces, including zero dimension and spaces not assumed complete. — The generalization is stated in the extraction and lesson and justified by restriction to real affine lines. No derivative of the ambient norm, volume construction or inner-product identity is required.
- assumptions: The source's 0<α≤β and upper Hessian bound are reduced to the lower derivative bound with arbitrary real α for this supporting implication only. — The proof needs only q''≥0 after subtracting c=α‖v‖². The α=0 and zero-dimensional arbitrary-α tests compile. Negative α is allowed in the chord convention but does not establish ordinary convexity or finite Gibbs normalization; source consumers retain their own positivity requirements.
- scopes: The implication is an attributed ASTIS mathematical expansion of the source Hessian assumptions, not an additional theorem claimed to appear in either paper. — Both primary Introduction (1.1) statements supply the C² Hessian-sandwich setting. The extraction, attribution and role prerequisite transparently identify the new supporting hessian-to-chord proof and no larger source conclusion.
- conclusion: Gibbs integrability, positive normalization, probability and RGO closure are verified downstream test consumers rather than additional production conclusions of this declaration. — Those tests add positive α and finite-dimensional Borel inner-product structure, then use separate compiled ASTIS theorems. No such measure-theoretic hypothesis or conclusion occurs in the Hessian adapter itself, and no sampler or process result is inferred.
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
- This is the supporting analytic meaning of the lower-Hessian part of the papers' C² potential assumptions, not either complete sampling theorem.
- The production theorem does not prove an upper-Hessian smoothness bound, a condition-number update, Gibbs integrability, a minimizer, an invariant kernel, output error or query complexity. Its tests exercise normalization and RGO consumers under their own required positive-modulus and finite-dimensional measure hypotheses.
- For a C² Euclidean potential, the source matrix inequality αI≼∇²V(x) means exactly the displayed diagonal quadratic-form lower bound. This declaration uses the canonical second Fréchet derivative, not an arbitrary field labelled Hessian, and does not introduce a coordinate-matrix representation API.
- The extension to any real normed space and arbitrary α concerns this analytic implication only. It is not an infinite-dimensional probability normalization or nonpositive-curvature sampling result.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
Mathlib API called (external library)
- ContDiff.differentiable
- ContDiff.fderiv_right
- ContDiff.differentiable_one
- HasFDerivAt.comp_hasDerivAt
- HasDerivAt.clm_apply
- HasDerivAt.pow
- HasDerivAt.const_mul
- HasDerivAt.sub
- convexOn_of_hasDerivWithinAt2_nonneg
- norm_sub_rev
Mathematical sources
- Chen, Chewi, Lu and Zhang, Smoothed Picard Hamiltonian Monte Carlo v1, Introduction (1.1) — The C² Euclidean potential and pointwise Hessian sandwich supply the source setting. The line-restriction proof is ASTIS's expanded supporting argument, not quoted source prose or full sampler formalization.
- Chen, Chewi, Lu and Zhang, Proximal Bouncy Particle Sampler v1, Introduction (1.1) — The same C² lower-Hessian assumption supplies a second consumer of this canonical shared analytic adapter.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.