ASTIS mathematical exposition

A convex smooth function has a Lipschitz gradient

AutoSamplingTheory.TechnicalLemmas.Analysis.ConvexSmoothGradient.gradient_lipschitz · theorem · Teaching coverage

Statement

For a nonnegative real β and a C¹ convex real-valued function on a complete real inner-product space satisfying the global β quadratic upper model, its genuine gradient is β-Lipschitz everywhere.

\[\begin{gathered}f(y)\le f(x)+\langle\nabla f(x),y-x\rangle+\frac\beta2\|y-x\|^2\\[4pt]B_f(y,x):=f(y)-f(x)-\langle\nabla f(x),y-x\rangle\\[4pt]\|\nabla f(y)-\nabla f(x)\|\le\beta\|y-x\|\end{gathered}\]

All objects and hypotheses

E is a complete real inner-product space, f:E→ℝ, and all points range over the entire space E.
f is C¹ (ContDiff ℝ 1 f) and convex on E (ConvexOn ℝ Set.univ f). No second derivative is assumed.
The genuine gradient is the Riesz representative of the Fréchet derivative. The displayed quadratic upper model holds for every x,y.
β:NNReal encodes exactly a nonnegative real number, including zero.

Mathematical proof

1. Combine cocoercivity with Cauchy–Schwarz

Write d=∇f(y)−∇f(x), v=y−x. Multiply the inner-product upper bound by the nonnegative β and combine it with cocoercivity.

\[\|d\|^2\le\beta\langle d,v\rangle\le\beta\|d\|\|v\|.\]

Corresponding Lean step

gradient_cocoercive and real_inner_le_norm; mul_le_mul_of_nonneg_left uses β.coe_nonneg.

2. Cancel only a positive gradient difference

If ‖d‖=0, the desired inequality is immediate. Otherwise ‖d‖>0 and cancellation yields the Lipschitz estimate. This does not divide by β and therefore includes β=0.

\[\|\nabla f(y)-\nabla f(x)\|\le\beta\|y-x\|\]

Corresponding Lean step

lipschitzWith_iff_norm_sub_le; by_cases on the norm, norm_nonneg, mul_le_mul_iff_left₀ and nlinarith.

Lean statement · gradient_lipschitz

For a nonnegative real β and a C¹ convex real-valued function on a complete real inner-product space satisfying the global β quadratic upper model, its genuine gradient is β-Lipschitz everywhere.

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_lipschitz {f : E → ℝ} {β : NNReal}
    (hf : ContDiff ℝ 1 f) (hc : ConvexOn ℝ univ f)
    (hu : ∀ x y, f y ≤ f x + inner ℝ (gradient f x) (y - x) + (β : ℝ) / 2 * ‖y - x‖ ^ 2) :
    LipschitzWith β (gradient f)

Exact module and namespace context

Lean proof · gradient_lipschitz

Write d=∇f(y)−∇f(x), v=y−x. Multiply the inner-product upper bound by the nonnegative β and combine it with cocoercivity. If ‖d‖=0, the desired inequality is immediate. Otherwise ‖d‖>0 and cancellation yields the Lipschitz estimate. This does not divide by β and therefore includes β=0.

theorem gradient_lipschitz {f : E → ℝ} {β : NNReal}
    (hf : ContDiff ℝ 1 f) (hc : ConvexOn ℝ univ f)
    (hu : ∀ x y, f y ≤ f x + inner ℝ (gradient f x) (y - x) + (β : ℝ) / 2 * ‖y - x‖ ^ 2) :
    LipschitzWith β (gradient f) := by
  rw [lipschitzWith_iff_norm_sub_le]
  intro x y
  have h := gradient_cocoercive hf hc β.coe_nonneg hu y x
  have hs := mul_le_mul_of_nonneg_left
    (real_inner_le_norm (gradient f x - gradient f y) (x - y)) β.coe_nonneg
  by_cases hz : ‖gradient f x - gradient f y‖ = 0
  · rw [hz]
    positivity
  · apply (mul_le_mul_iff_left₀ (lt_of_le_of_ne (norm_nonneg _) (Ne.symm hz))).mp
    nlinarith

end AutoSamplingTheory.TechnicalLemmas.Analysis.ConvexSmoothGradient

Exact module and namespace context

Scope and omitted-condition boundaries

The complete real inner-product space explicitly generalizes the source Euclidean space. A constrained set is not covered: the trial gradient step must remain in the domain. No Riemannian, stochastic, or companion-paper theorem is claimed.
Definition1.12 permits β≥0, but the reciprocal in (3.4) and the suggested step 1/β require β>0; the source does not state that restriction explicitly. The first declaration covers this positive domain. The scaled (3.5) and Lipschitz conclusions are separately established at β=0.

Source and reuse

ASTIS parents called

AutoSamplingTheory.TechnicalLemmas.Analysis.ConvexSmoothGradient.gradient_cocoercive

Mathlib API called (external library)

lipschitzWith_iff_norm_sub_le; real_inner_le_norm
mul_le_mul_of_nonneg_left; mul_le_mul_iff_left₀; norm_nonneg

Mathematical sources

Sinho Chewi, Exercise3.1 (3.4)-(3.5) — ASTIS-authored explanation of the tangent-plane descent route and explicit zero-modulus extension.
Pinned Optlib convex_to_lower / lower_to_lipschitz — External mathematical reuse provenance, Apache-2.0; not an imported compiled dependency.
Reciprocal formula, zero modulus and nonexpansive gradient-step consumers — Compiled use of the actual declarations.

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