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

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 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.