ConvexityC1: 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 gradient along a segment
Recover the chord inequality by integration
The three C¹ convexity conditions are equivalent

ASTIS mathematical exposition

Integrate the gradient along a segment

AutoSamplingTheory.TechnicalLemmas.Analysis.ConvexityC1.sub_eq_integral_gradient · theorem · Teaching coverage

Statement

For every x,v in a complete real inner-product space and every C¹ real-valued f, the difference f(x+v)−f(x) equals the integral of the gradient pairing along that segment.

\[f(x+v)-f(x)=\int_0^1\langle\nabla f(x+sv),v\rangle\,ds.\]

All objects and hypotheses

E is a complete real inner-product space and f:E→ℝ is continuously Fréchet differentiable on all E.
gradient f is the genuine gradient supplied by C¹, not an unsupported totalized derivative.
x,v∈E are arbitrary, including v=0; the integral is with respect to Lebesgue measure on [0,1].

Mathematical proof

1. Differentiate the affine segment

C¹ gives a genuine derivative of f at every point. The chain rule differentiates the composition with x+sv, including the two endpoints.

\[\frac{d}{ds}f(x+sv)=\langle\nabla f(x+sv),v\rangle.\]

Corresponding Lean step

hd: DifferentiableAt.hasGradientAt, HasFDerivAt.comp_hasDerivAt and the derivative of x+s•v.

2. Establish integrability, then apply FTC

The derivative map is continuous because f is C¹. Evaluating it on the fixed direction v and composing with the segment gives a continuous scalar integrand; compact-interval integrability follows. FTC and the values at 0 and 1 give the identity.

\[\int_0^1\frac{d}{ds}f(x+sv)\,ds=f(x+v)-f(x).\]

Corresponding Lean step

hc uses ContDiff.continuous_fderiv and Continuous.clm_apply; Continuous.intervalIntegrable and intervalIntegral.integral_eq_sub_of_hasDerivAt finish.

Lean statement · sub_eq_integral_gradient

For every x,v in a complete real inner-product space and every C¹ real-valued f, the difference f(x+v)−f(x) equals the integral of the gradient pairing along that segment.

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

Exact module and namespace context

Lean proof · sub_eq_integral_gradient

C¹ gives a genuine derivative of f at every point. The chain rule differentiates the composition with x+sv, including the two endpoints. The derivative map is continuous because f is C¹. Evaluating it on the fixed direction v and composing with the segment gives a continuous scalar integrand; compact-interval integrability follows. FTC and the values at 0 and 1 give the identity.

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

/-- Quantitative gradient monotonicity implies the chord inequality by the
source's two affine-segment FTC identities and integration of their difference.
The modulus can be signed; no Hessian or extra integrability is assumed. -/

Exact module and namespace context

Scope and omitted-condition boundaries

A reusable Hilbert-space generalization of the segment identity used in the source; no convexity, Hessian, infinite-time integral or measure on E is asserted.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

ContDiff.continuous_fderiv; Continuous.clm_apply; InnerProductSpace.toDual_symm_apply
DifferentiableAt.hasGradientAt; HasFDerivAt.comp_hasDerivAt
Continuous.intervalIntegrable; intervalIntegral.integral_eq_sub_of_hasDerivAt

Mathematical sources

Sinho Chewi, Proposition 1.6 part 1 — ASTIS-authored statement and explanation of the selected proof boundary.
Focused mathematical consumers — Reversed segment, signed quadratic, stationary-point growth and zero-dimension tests.

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

Recover the chord inequality by integration

AutoSamplingTheory.TechnicalLemmas.Analysis.ConvexityC1.strongConvexOn_univ_of_gradient_mono_integral · theorem · Teaching coverage

Statement

For C¹ f on a complete real inner-product space, a global gradient monotonicity lower bound with any real modulus m implies StrongConvexOn univ m f.

\[\langle\nabla f(y)-\nabla f(x),y-x\rangle\ge m\|y-x\|^2\ \Longrightarrow\ f((1-t)x+ty)\le(1-t)f(x)+tf(y)-\frac m2t(1-t)\|y-x\|^2.\]

All objects and hypotheses

E is a complete real inner-product space and f:E→ℝ is continuously Fréchet differentiable on all E.
gradient f is the genuine gradient supplied by C¹, not an unsupported totalized derivative.
m∈ℝ may be negative, zero or positive. For all x,y∈E, the displayed gradient lower bound holds.
The conclusion includes every x,y and every t∈[0,1].

Mathematical proof

1. Compare two segment integrals

Put v=y−x and fix 0≤t≤1. Apply the segment identity to v and to tv. Scalar linearity moves t outside the second integral.

\[A(s)=\langle\nabla f(x+sv),v\rangle,\quad B(s)=\langle\nabla f(x+stv),v\rangle;\quad f(y)-f(x)=\int_0^1A(s)ds,\quad f(x+tv)-f(x)=t\int_0^1B(s)ds.\]

Corresponding Lean step

hy and hz invoke sub_eq_integral_gradient twice; smul_smul, inner_smul_right and integral_const_mul expose A and B.

2. Cancel a strictly positive displacement parameter

The case t=1 is equality. For t<1 and 0<s<1, the difference of the two segment points is s(1−t)v. Apply gradient monotonicity and cancel s(1−t)>0. No division occurs at a zero displacement parameter.

\[A(s)-B(s)\ge m s(1-t)\|v\|^2.\]

Corresponding Lean step

hdis and hscaled rewrite the gradient hypothesis; le_of_mul_le_mul_left uses mul_pos hs.1 (sub_pos.mpr ht1).

3. Integrate the lower bound

C¹ makes A and B continuous and hence interval integrable. The inequality on the open interval suffices because Lebesgue measure gives its endpoints zero mass. Integrate s from 0 to 1.

\[\int_0^1(A-B)\,ds\ge\frac m2(1-t)\|v\|^2.\]

Corresponding Lean step

integral_mono_on_of_le_Ioo, Continuous.intervalIntegrable, integral_sub, integral_id and scalar integral linearity.

4. Restore the chord residual

Multiply the integrated lower bound by nonnegative t and substitute the two FTC identities. This gives the exact m/2 correction; it also covers t=0. The signed m is never divided by or required to be positive.

\[f(x+tv)-(1-t)f(x)-tf(y)=-t\int_0^1(A-B)\,ds\le-\frac m2t(1-t)\|v\|^2.\]

Corresponding Lean step

hpoint matches affine conventions; mul_le_mul_of_nonneg_left and ring arithmetic conclude StrongConvexOn.

Lean statement · strongConvexOn_univ_of_gradient_mono_integral

For C¹ f on a complete real inner-product space, a global gradient monotonicity lower bound with any real modulus m implies StrongConvexOn univ m f.

theorem strongConvexOn_univ_of_gradient_mono_integral
    {f : E → ℝ} {m : ℝ} (hf : ContDiff ℝ 1 f)
    (hm : ∀ x y : E, m * ‖y - x‖ ^ 2 ≤
      inner ℝ (gradient f y - gradient f x) (y - x)) :
    StrongConvexOn (univ : Set E) m f

Exact module and namespace context

Lean proof · strongConvexOn_univ_of_gradient_mono_integral

Put v=y−x and fix 0≤t≤1. Apply the segment identity to v and to tv. Scalar linearity moves t outside the second integral. The case t=1 is equality. For t<1 and 0<s<1, the difference of the two segment points is s(1−t)v. Apply gradient monotonicity and cancel s(1−t)>0. No division occurs at a zero displacement parameter. C¹ makes A and B continuous and hence interval integrable. The inequality on the open interval suffices because Lebesgue measure gives its endpoints zero mass. Integrate s from 0 to 1. Multiply the integrated lower bound by nonnegative t and substitute the two FTC identities. This gives the exact m/2 correction; it also covers t=0. The signed m is never divided by or required to be positive.

theorem strongConvexOn_univ_of_gradient_mono_integral
    {f : E → ℝ} {m : ℝ} (hf : ContDiff ℝ 1 f)
    (hm : ∀ x y : E, m * ‖y - x‖ ^ 2 ≤
      inner ℝ (gradient f y - gradient f x) (y - x)) :
    StrongConvexOn (univ : Set E) m f := by
  refine ⟨convex_univ, ?_⟩
  intro x _ y _ a t ha ht hat
  have hat' : a = 1 - t := by linarith
  subst a
  have ht1 : t ≤ 1 := by linarith
  rcases eq_or_lt_of_le ht1 with ht1 | ht1
  · subst t
    simp
  let v := y - x
  let A : ℝ → ℝ := fun s => inner ℝ (gradient f (x + s • v)) v
  let B : ℝ → ℝ := fun s => inner ℝ (gradient f (x + (s * t) • v)) v
  have hA : Continuous A := by
    simpa [A, gradient, Function.comp_def] using
      ((hf.continuous_fderiv (by norm_num)).comp
        (continuous_const.add (continuous_id.smul continuous_const))).clm_apply continuous_const
  have hB : Continuous B := by
    simpa [B, gradient, Function.comp_def] using
      ((hf.continuous_fderiv (by norm_num)).comp
        (continuous_const.add ((continuous_id.mul continuous_const).smul continuous_const))).clm_apply continuous_const
  have hbound : ∫ s : ℝ in 0..1, m * s * (1 - t) * ‖v‖ ^ 2 ≤
      ∫ s : ℝ in 0..1, (A s - B s) := by
    apply intervalIntegral.integral_mono_on_of_le_Ioo (by norm_num)
      ((show Continuous (fun s : ℝ => m * s * (1 - t) * ‖v‖ ^ 2) by fun_prop).intervalIntegrable 0 1)
      ((hA.sub hB).intervalIntegrable 0 1)
    intro s hs
    have h := hm (x + (s * t) • v) (x + s • v)
    have hdis : (x + s • v) - (x + (s * t) • v) = (s * (1 - t)) • v := by module
    rw [hdis, norm_smul, Real.norm_eq_abs, mul_pow, sq_abs, inner_smul_right] at h
    have hscaled : (s * (1 - t)) * (m * s * (1 - t) * ‖v‖ ^ 2) ≤
        (s * (1 - t)) * inner ℝ
          (gradient f (x + s • v) - gradient f (x + (s * t) • v)) v := by nlinarith [h]
    have hcancel := le_of_mul_le_mul_left hscaled (mul_pos hs.1 (sub_pos.mpr ht1))
    simpa [A, B, inner_sub_left] using hcancel
  have hpoly : (∫ s : ℝ in 0..1, m * s * (1 - t) * ‖v‖ ^ 2) =
      m / 2 * (1 - t) * ‖v‖ ^ 2 := by
    rw [intervalIntegral.integral_mul_const, intervalIntegral.integral_mul_const,
      intervalIntegral.integral_const_mul, integral_id]
    norm_num only [one_pow, zero_pow, sub_zero]
    ring
  rw [hpoly, intervalIntegral.integral_sub (hA.intervalIntegrable 0 1)
    (hB.intervalIntegrable 0 1)] at hbound
  have hy := sub_eq_integral_gradient hf x v
  have hz := sub_eq_integral_gradient hf x (t • v)
  have hpoint : (1 - t) • x + t • y = x + t • v := by dsimp [v]; module
  have hys : x + v = y := by simp [v]
  rw [hys] at hy
  change f y - f x = ∫ s : ℝ in 0..1, A s at hy
  simp only [smul_smul, inner_smul_right, intervalIntegral.integral_const_mul] at hz
  change f (x + t • v) - f x = t * ∫ s : ℝ in 0..1, B s at hz
  change f ((1 - t) • x + t • y) ≤ (1 - t) * f x + t * f y -
    (1 - t) * t * (m / 2 * ‖x - y‖ ^ 2)
  rw [hpoint, norm_sub_rev]
  change f (x + t • v) ≤ (1 - t) * f x + t * f y -
    (1 - t) * t * (m / 2 * ‖v‖ ^ 2)
  nlinarith [mul_le_mul_of_nonneg_left hbound ht]

/-- Proposition 1.6, part 1: on all of Euclidean space, the C¹ chord,
quadratic lower-model and gradient-monotonicity conditions are equivalent.
The nonnegative modulus is retained exactly as in the source. -/

Exact module and namespace context

Scope and omitted-condition boundaries

This follows the source integral route, generalized to complete real inner-product spaces and signed m. It is distinct from the previously published MVT converse.
No C²/Hessian characterization or convergence result is claimed.

Source and reuse

ASTIS parents called

AutoSamplingTheory.TechnicalLemmas.Analysis.ConvexityC1.sub_eq_integral_gradient

Mathlib API called (external library)

intervalIntegral.integral_mono_on_of_le_Ioo; Continuous.intervalIntegrable
intervalIntegral.integral_sub, integral_const_mul, integral_mul_const; integral_id
norm_smul; inner_smul_right; inner_sub_left; le_of_mul_le_mul_left

Mathematical sources

Sinho Chewi, Proposition 1.6 part 1 — ASTIS-authored statement and explanation of the selected proof boundary.
Focused mathematical consumers — Reversed segment, signed quadratic, stationary-point growth and zero-dimension tests.

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

The three C¹ convexity conditions are equivalent

AutoSamplingTheory.TechnicalLemmas.Analysis.ConvexityC1.convexity_equivalences · theorem · Teaching coverage

Statement

Let d be a natural number, f:ℝᵈ→ℝ be C¹ on all Euclidean space, and m≥0. The strong-convexity chord inequality is equivalent both to the global quadratic lower model and to the quantitative gradient monotonicity inequality.

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

All objects and hypotheses

d∈ℕ; E=EuclideanSpace ℝ (Fin d), with its standard Euclidean inner product and norm. Zero dimension is allowed.
f:E→ℝ is C¹ on all E, and m∈ℝ satisfies m≥0, exactly the source parameter restriction.
All x,y are universally quantified over E; the chord condition includes every nonnegative pair of weights summing to one.

Mathematical proof

1. Obtain the first-order model

C¹ supplies the ambient gradients everywhere. Apply the already compiled shared lower-model theorem, whose proof takes the derivative limit of the strong-convexity chord inequality.

\[\mathrm{StrongConvex}_m(f)\Rightarrow f(y)\ge f(x)+\langle\nabla f(x),y-x\rangle+\frac m2\|y-x\|^2.\]

Corresponding Lean step

hg derives HasGradientAt from hf; hforward calls StrongConvexFirstOrder.firstOrder_lower_bound_of_strongConvexOn on univ.

2. Add the two endpoint models

Assume only the global lower-model condition, apply it in both orders, and add. Function values cancel, the two half-quadratic terms add, and the inner products combine into a gradient difference.

\[m\|y-x\|^2\le\langle\nabla f(y)-\nabla f(x),y-x\rangle.\]

Corresponding Lean step

hsum rewrites x−y=−(y−x), inner_neg_right and inner_sub_left, then uses linear arithmetic.

3. Close the cycle with the source integral argument

The newly proved integral converse takes gradient monotonicity back to the chord condition. Package the two equivalences using this three-condition cycle.

\[(1.3)\Rightarrow(1.4)\Rightarrow(1.5)\Rightarrow(1.3).\]

Corresponding Lean step

strongConvexOn_univ_of_gradient_mono_integral closes both reverse directions. The final statement is the conjunction of the two iff results.

Lean statement · convexity_equivalences

theorem convexity_equivalences {d : ℕ} {f : EuclideanSpace ℝ (Fin d) → ℝ}
    {m : ℝ} (_hm : 0 ≤ m) (hf : ContDiff ℝ 1 f) :
    (StrongConvexOn univ m f ↔ ∀ x y,
      f x + inner ℝ (gradient f x) (y - x) + m / 2 * ‖y - x‖ ^ 2 ≤ f y) ∧
    (StrongConvexOn univ m f ↔ ∀ x y,
      m * ‖y - x‖ ^ 2 ≤ inner ℝ (gradient f y - gradient f x) (y - x))

Exact module and namespace context

Lean proof · convexity_equivalences

C¹ supplies the ambient gradients everywhere. Apply the already compiled shared lower-model theorem, whose proof takes the derivative limit of the strong-convexity chord inequality. Assume only the global lower-model condition, apply it in both orders, and add. Function values cancel, the two half-quadratic terms add, and the inner products combine into a gradient difference. The newly proved integral converse takes gradient monotonicity back to the chord condition. Package the two equivalences using this three-condition cycle.

theorem convexity_equivalences {d : ℕ} {f : EuclideanSpace ℝ (Fin d) → ℝ}
    {m : ℝ} (_hm : 0 ≤ m) (hf : ContDiff ℝ 1 f) :
    (StrongConvexOn univ m f ↔ ∀ x y,
      f x + inner ℝ (gradient f x) (y - x) + m / 2 * ‖y - x‖ ^ 2 ≤ f y) ∧
    (StrongConvexOn univ m f ↔ ∀ x y,
      m * ‖y - x‖ ^ 2 ≤ inner ℝ (gradient f y - gradient f x) (y - x)) := by
  have hg : ∀ z ∈ (univ : Set (EuclideanSpace ℝ (Fin d))),
      HasGradientAt f (gradient f z) z := fun z _ => (hf.differentiable_one z).hasGradientAt
  have hforward := fun (hsc : StrongConvexOn univ m f) x y =>
    StrongConvexFirstOrder.firstOrder_lower_bound_of_strongConvexOn hsc hg
      (mem_univ x) (mem_univ y)
  have hsum : (∀ x y, f x + inner ℝ (gradient f x) (y - x) +
      m / 2 * ‖y - x‖ ^ 2 ≤ f y) → ∀ x y,
      m * ‖y - x‖ ^ 2 ≤ inner ℝ (gradient f y - gradient f x) (y - x) := by
    intro hl x y
    have hxy := hl x y
    have hyx := hl y x
    rw [show x - y = -(y - x) by abel, inner_neg_right, norm_neg] at hyx
    rw [inner_sub_left]
    linarith
  exact ⟨⟨hforward, fun h => strongConvexOn_univ_of_gradient_mono_integral hf (hsum h)⟩,
    ⟨fun h => hsum (hforward h), strongConvexOn_univ_of_gradient_mono_integral hf⟩⟩

end AutoSamplingTheory.TechnicalLemmas.Analysis.ConvexityC1

Exact module and namespace context

Scope and omitted-condition boundaries

Exactly Proposition 1.6 part 1. The separate ConvexityC2.strongConvexOn_iff_fderiv2_lower declaration now supplies the C²/Hessian equivalence; this declaration itself covers only the C¹ conditions.
The declaration retains m≥0 even though its shared parents also handle signed m. No new convexity definition or caller-supplied gradient is introduced.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

ContDiff.differentiable_one; DifferentiableAt.hasGradientAt
inner_neg_right; inner_sub_left; norm_neg

Mathematical sources

Sinho Chewi, Proposition 1.6 part 1 — ASTIS-authored statement and explanation of the selected proof boundary.
Focused mathematical consumers — Reversed segment, signed quadratic, stationary-point growth and zero-dimension tests.

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