ASTIS mathematical exposition

C² strong convexity is equivalent to the Hessian bound

AutoSamplingTheory.TechnicalLemmas.Analysis.ConvexityC2.strongConvexOn_iff_fderiv2_lower · theorem · Teaching coverage

Statement

For every natural dimension d, every nonnegative real m and every C² f on all Euclidean d-space, f is m-strongly convex if and only if its Hessian quadratic form is at least m times squared norm in every direction at every point.

\[\mathrm{StrongConvex}_m(f)\quad\Longleftrightarrow\quad\forall x,v\in\mathbb R^d,\ D^2f(x)[v,v]\ge m\|v\|^2.\]

All objects and hypotheses

d∈ℕ and E=EuclideanSpace ℝ (Fin d), with its standard real inner product and norm; d=0 is allowed.
f:E→ℝ is C² on all E and m∈ℝ satisfies m≥0, exactly as in the source.
StrongConvexOn univ m f uses the chord correction (m/2)t(1−t)‖y−x‖² for all x,y and t∈[0,1]. D²f is the genuine second derivative, written as a bilinear evaluation.

Mathematical proof

1. Reuse the C¹ equivalence

C² implies C¹. Apply the already proved source equivalence between the chord condition and global gradient monotonicity.

\[\mathrm{StrongConvex}_m(f)\Longleftrightarrow\forall x,y,\ \langle\nabla f(y)-\nabla f(x),y-x\rangle\ge m\|y-x\|^2.\]

Corresponding Lean step

ContDiff.of_le supplies C¹; ConvexityC1.convexity_equivalences supplies its second iff.

2. Join the Hessian equivalence

Compose with the derivative-limit/integral equivalence above. On Euclidean space D²f(x)[v,v] is the source Hessian matrix quadratic form. This finishes part 2 and connects it to the lower-model equivalence already in part 1.

\[\text{chord}\Longleftrightarrow\text{gradient monotonicity}\Longleftrightarrow\text{Hessian lower bound}.\]

Corresponding Lean step

Iff.trans with gradient_mono_iff_fderiv2_lower. No alternative assumed convexity or gradient interface is substituted.

Lean statement · strongConvexOn_iff_fderiv2_lower

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_iff_fderiv2_lower
    {d : ℕ} {f : EuclideanSpace ℝ (Fin d) → ℝ} {m : ℝ}
    (hm : 0 ≤ m) (hf : ContDiff ℝ 2 f) :
    StrongConvexOn univ m f ↔
      ∀ x v, m * ‖v‖ ^ 2 ≤ (fderiv ℝ (fderiv ℝ f) x v) v

Exact module and namespace context

Lean proof · strongConvexOn_iff_fderiv2_lower

C² implies C¹. Apply the already proved source equivalence between the chord condition and global gradient monotonicity. Compose with the derivative-limit/integral equivalence above. On Euclidean space D²f(x)[v,v] is the source Hessian matrix quadratic form. This finishes part 2 and connects it to the lower-model equivalence already in part 1.

theorem strongConvexOn_iff_fderiv2_lower
    {d : ℕ} {f : EuclideanSpace ℝ (Fin d) → ℝ} {m : ℝ}
    (hm : 0 ≤ m) (hf : ContDiff ℝ 2 f) :
    StrongConvexOn univ m f ↔
      ∀ x v, m * ‖v‖ ^ 2 ≤ (fderiv ℝ (fderiv ℝ f) x v) v := by
  exact (ConvexityC1.convexity_equivalences hm (hf.of_le (by norm_num))).2.trans
    (gradient_mono_iff_fderiv2_lower hf)

end AutoSamplingTheory.TechnicalLemmas.Analysis.ConvexityC2

Exact module and namespace context

Scope and omitted-condition boundaries

Exact Proposition 1.6 part 2; part 1 remains provided by the unchanged C¹ theorem. This does not complete the chapter or assert a Riemannian analogue.
Earlier first-order leaves retain their explicitly recorded historical review debt; this result does not rewrite their audit history.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

ContDiff.of_le; Iff.trans

Mathematical sources

Sinho Chewi, Proposition 1.6 part 2 — ASTIS-authored explanation of the pinned source proof.
Focused consumers and boundary cases — Checks the actual declarations and their composition.

ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.