ConvexityC2: mathematical reading route

Read the statements and derivations in source order. Every result has its own optional Lean statement and proof. Source assumptions, library reuse and unproved boundaries are kept explicit.

Integrate the Hessian along a segment
Gradient monotonicity is equivalent to a Hessian lower bound
C² strong convexity is equivalent to the Hessian bound

ASTIS mathematical exposition

Integrate the Hessian along a segment

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

Statement

For every C² real-valued f on a complete real inner-product space and every x,v, the gradient difference between x+v and x, paired with v, equals the integral of the Hessian quadratic form along that segment.

\[\langle\nabla f(x+v)-\nabla f(x),v\rangle=\int_0^1 D^2f(x+tv)[v,v]\,dt.\]

All objects and hypotheses

E is a complete real inner-product space; f:E→ℝ is twice continuously Fréchet differentiable everywhere.
The Hessian quadratic form means the genuine second derivative D²f(x)[v,v]=(fderiv ℝ (fderiv ℝ f) x v) v. The pairing with the actual gradient equals Df(x)[v].
x,v∈E are arbitrary, including v=0. The integral uses real Lebesgue measure on [0,1].

Mathematical proof

1. Differentiate the scalar gradient pairing

Set g(t)=Df(x+tv)[v]. Because f is C², Df is C¹; compose its derivative with the affine segment and evaluate the resulting linear functional at the fixed v.

\[g(t)=Df(x+tv)[v],\qquad g^{\prime}(t)=D^2f(x+tv)[v,v].\]

Corresponding Lean step

hfd uses ContDiff.fderiv_right. hd uses HasFDerivAt.comp_hasDerivAt and HasDerivAt.clm_apply.

2. Integrate the genuine derivative

The second derivative is continuous. Composition with the segment and two evaluations preserve continuity, giving interval integrability. FTC gives g(1)−g(0). The gradient pairing identity identifies the endpoints.

\[\int_0^1g^{\prime}(t)\,dt=g(1)-g(0)=\langle\nabla f(x+v)-\nabla f(x),v\rangle.\]

Corresponding Lean step

hc: ContDiff.continuous_fderiv and Continuous.clm_apply; Continuous.intervalIntegrable and intervalIntegral.integral_eq_sub_of_hasDerivAt; gradient/Riesz simplification.

Lean statement · gradient_sub_inner_eq_integral_fderiv2

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 gradient_sub_inner_eq_integral_fderiv2
    {f : E → ℝ} (hf : ContDiff ℝ 2 f) (x v : E) :
    inner ℝ (gradient f (x + v) - gradient f x) v =
      ∫ t : ℝ in 0..1, (fderiv ℝ (fderiv ℝ f) (x + t • v) v) v

Exact module and namespace context

Lean proof · gradient_sub_inner_eq_integral_fderiv2

Set g(t)=Df(x+tv)[v]. Because f is C², Df is C¹; compose its derivative with the affine segment and evaluate the resulting linear functional at the fixed v. The second derivative is continuous. Composition with the segment and two evaluations preserve continuity, giving interval integrability. FTC gives g(1)−g(0). The gradient pairing identity identifies the endpoints.

theorem gradient_sub_inner_eq_integral_fderiv2
    {f : E → ℝ} (hf : ContDiff ℝ 2 f) (x v : E) :
    inner ℝ (gradient f (x + v) - gradient f x) v =
      ∫ t : ℝ in 0..1, (fderiv ℝ (fderiv ℝ f) (x + t • v) v) v := by
  have hfd : ContDiff ℝ 1 (fderiv ℝ f) := hf.fderiv_right (by norm_num)
  have hd (t : ℝ) : HasDerivAt (fun s : ℝ => fderiv ℝ f (x + s • v) v)
      ((fderiv ℝ (fderiv ℝ f) (x + t • v) v) v) t := by
    convert ((hfd.differentiable_one _).hasFDerivAt.comp_hasDerivAt t
      (((hasDerivAt_id t).smul_const v).const_add x)).clm_apply
      (hasDerivAt_const t v) using 1 <;> first | rfl | simp
  have hc : Continuous (fun t : ℝ => (fderiv ℝ (fderiv ℝ f) (x + t • v) v) v) :=
    (((hfd.continuous_fderiv (by norm_num)).comp
      (continuous_const.add (continuous_id.smul continuous_const))).clm_apply
        continuous_const).clm_apply continuous_const
  simpa [inner_sub_left, gradient, Function.comp_def] using
    (intervalIntegral.integral_eq_sub_of_hasDerivAt
      (fun t _ => hd t) (hc.intervalIntegrable 0 1)).symm

/-- Global quantitative gradient monotonicity is equivalent to the genuine
Hessian diagonal lower bound, by a right derivative limit and the FTC. -/

Exact module and namespace context

Scope and omitted-condition boundaries

The source segment identity generalized from Euclidean space to complete real inner-product space. No convexity or Hessian bound is assumed.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

ContDiff.fderiv_right; ContDiff.differentiable_one; ContDiff.continuous_fderiv
HasFDerivAt.comp_hasDerivAt; HasDerivAt.clm_apply; Continuous.clm_apply
Continuous.intervalIntegrable; intervalIntegral.integral_eq_sub_of_hasDerivAt; InnerProductSpace.toDual_symm_apply

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.

ASTIS mathematical exposition

Gradient monotonicity is equivalent to a Hessian lower bound

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

Statement

For C² f on a complete real inner-product space and any real m, the global quantitative gradient monotonicity inequality is equivalent to D²f(x)[v,v]≥m‖v‖² at every point and direction.

\[\bigl[\forall x,y,\ \langle\nabla f(y)-\nabla f(x),y-x\rangle\ge m\|y-x\|^2\bigr]\ \Longleftrightarrow\ \bigl[\forall x,v,\ D^2f(x)[v,v]\ge m\|v\|^2\bigr].\]

All objects and hypotheses

E is a complete real inner-product space; f:E→ℝ is twice continuously Fréchet differentiable everywhere.
The Hessian quadratic form means the genuine second derivative D²f(x)[v,v]=(fderiv ℝ (fderiv ℝ f) x v) v. The pairing with the actual gradient equals Df(x)[v].
m is any real number; all x,y and v range over all E. No positivity of m or nonzero direction is required.

Mathematical proof

1. Use a positive directional increment

\[t^2m\|v\|^2\le t(g(t)-g(0)),\qquad m\|v\|^2\le\frac{g(t)-g(0)}t.\]

Corresponding Lean step

hm, norm_smul, sq_abs and inner_smul_right give h; le_of_mul_le_mul_left and le_div_iff₀ cancel only ht:0<t.

2. Pass to the right derivative

C² gives g′(0)=D²f(x)[v,v]. The displayed inequality holds for all positive t, so passage to t↓0 preserves it. Neither m nor ‖v‖ is divided by.

\[m\|v\|^2\le\lim_{t\downarrow0}\frac{g(t)-g(0)}t=D^2f(x)[v,v].\]

Corresponding Lean step

hdAll and hd establish the genuine scalar derivative; HasDerivAt.tendsto_slope_zero_right and ge_of_tendsto pass to the limit.

3. Integrate the Hessian lower bound for the converse

For v=y−x the Hessian bound holds along x+tv. C² gives a continuous integrand and interval integrability. Integrate the constant lower bound over an interval of length one, then use the preceding segment identity.

\[\langle\nabla f(y)-\nabla f(x),v\rangle=\int_0^1D^2f(x+tv)[v,v]dt\ge\int_0^1m\|v\|^2dt=m\|v\|^2.\]

Corresponding Lean step

intervalIntegral.integral_mono_on compares integrals; gradient_sub_inner_eq_integral_fderiv2 identifies the result.

Lean statement · gradient_mono_iff_fderiv2_lower

For C² f on a complete real inner-product space and any real m, the global quantitative gradient monotonicity inequality is equivalent to D²f(x)[v,v]≥m‖v‖² at every point and direction.

theorem gradient_mono_iff_fderiv2_lower
    {f : E → ℝ} {m : ℝ} (hf : ContDiff ℝ 2 f) :
    (∀ x y : E, m * ‖y - x‖ ^ 2 ≤
      inner ℝ (gradient f y - gradient f x) (y - x)) ↔
    ∀ x v : E, m * ‖v‖ ^ 2 ≤ (fderiv ℝ (fderiv ℝ f) x v) v

Exact module and namespace context

Lean proof · gradient_mono_iff_fderiv2_lower

Fix x,v and let g(t)=Df(x+tv)[v]. Apply gradient monotonicity at x and x+tv with t>0. The displacement is tv and its squared norm is t²‖v‖². Cancelling the positive t and dividing once more by t gives a bound on the difference quotient. C² gives g′(0)=D²f(x)[v,v]. The displayed inequality holds for all positive t, so passage to t↓0 preserves it. Neither m nor ‖v‖ is divided by. For v=y−x the Hessian bound holds along x+tv. C² gives a continuous integrand and interval integrability. Integrate the constant lower bound over an interval of length one, then use the preceding segment identity.

theorem gradient_mono_iff_fderiv2_lower
    {f : E → ℝ} {m : ℝ} (hf : ContDiff ℝ 2 f) :
    (∀ x y : E, m * ‖y - x‖ ^ 2 ≤
      inner ℝ (gradient f y - gradient f x) (y - x)) ↔
    ∀ x v : E, m * ‖v‖ ^ 2 ≤ (fderiv ℝ (fderiv ℝ f) x v) v := by
  have hfd : ContDiff ℝ 1 (fderiv ℝ f) := hf.fderiv_right (by norm_num)
  constructor
  · intro hm x v
    let g : ℝ → ℝ := fun t => fderiv ℝ f (x + t • v) v
    have hdAll (t : ℝ) : HasDerivAt g
        ((fderiv ℝ (fderiv ℝ f) (x + t • v) v) v) t := by
      convert ((hfd.differentiable_one _).hasFDerivAt.comp_hasDerivAt t
        (((hasDerivAt_id t).smul_const v).const_add x)).clm_apply
        (hasDerivAt_const t v) using 1 <;> first | rfl | simp
    have hd : HasDerivAt g ((fderiv ℝ (fderiv ℝ f) x v) v) 0 := by
      simpa using hdAll 0
    apply ge_of_tendsto hd.tendsto_slope_zero_right
    filter_upwards [self_mem_nhdsWithin] with t ht
    have ht : 0 < t := ht
    have h := hm x (x + t • v)
    rw [add_sub_cancel_left, norm_smul, Real.norm_eq_abs, mul_pow, sq_abs,
      inner_smul_right, inner_sub_left] at h
    have hscaled : t * (m * ‖v‖ ^ 2) ≤ g t - g 0 := by
      apply le_of_mul_le_mul_left (a := t) _ ht
      simpa [g, gradient, Function.comp_def, pow_two, mul_assoc, mul_left_comm, mul_comm] using h
    simpa [smul_eq_mul, div_eq_inv_mul] using
      (le_div_iff₀ ht).mpr (by simpa [mul_comm] using hscaled)
  · intro hH x y
    let v := y - x
    have hc : Continuous (fun t : ℝ => (fderiv ℝ (fderiv ℝ f) (x + t • v) v) v) :=
      (((hfd.continuous_fderiv (by norm_num)).comp
        (continuous_const.add (continuous_id.smul continuous_const))).clm_apply
          continuous_const).clm_apply continuous_const
    have h := intervalIntegral.integral_mono_on (by norm_num : (0 : ℝ) ≤ 1)
      (intervalIntegrable_const : IntervalIntegrable (fun _ : ℝ => m * ‖v‖ ^ 2) volume 0 1)
      (hc.intervalIntegrable 0 1) (fun t _ => hH (x + t • v) v)
    rw [← gradient_sub_inner_eq_integral_fderiv2 hf x v] at h
    simpa [v] using h

/-- Proposition 1.6 part 2, with the source's whole Euclidean domain,
nonnegative modulus and C² regularity. Together with the C¹ theorem this
connects all four source conditions. -/

Exact module and namespace context

Scope and omitted-condition boundaries

The two directions follow the source derivative-limit and Hessian-integral routes. The complete-space and signed-modulus scope is an explicit generalization.
No independent Hessian field, symmetry assumption, measure on E or supplied integrability premise is introduced.

Source and reuse

ASTIS parents called

AutoSamplingTheory.TechnicalLemmas.Analysis.ConvexityC2.gradient_sub_inner_eq_integral_fderiv2

Mathlib API called (external library)

ContDiff.fderiv_right; HasFDerivAt.comp_hasDerivAt; HasDerivAt.clm_apply
HasDerivAt.tendsto_slope_zero_right; ge_of_tendsto; self_mem_nhdsWithin
intervalIntegral.integral_mono_on; Continuous.intervalIntegrable; intervalIntegral.integral_const

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.

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

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.