From a genuine Hessian lower bound to strong convexity
AutoSamplingTheory.TechnicalLemmas.Analysis.HessianStrongConvexity.strongConvexOn_univ_of_fderiv2_lower · theorem · Teaching coverage
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.
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 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) α VLean 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.HessianStrongConvexityScope 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.
Source and reuse
ASTIS 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.
ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.