Recover strong convexity from gradient separation
AutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexGradientConverse.strongConvexOn_of_gradient_inner_lower_bound · theorem · Teaching coverage
Statement
On a convex subset of a complete real inner-product space, a quantitative lower bound on differences of genuine gradients forces the matching strong-convexity chord inequality.
All objects and hypotheses
- E is a complete real inner-product space, s is a convex subset of E, f:E→ℝ, g:E→E and m∈ℝ.
- At every z∈s, g(z) is a genuine ambient gradient: HasGradientAt f (g z) z. This includes boundary points, and implies the continuity needed at segment endpoints.
- For every x,y∈s, the gradient difference paired with y−x is at least m‖y−x‖². The modulus may be positive, zero or negative.
- The conclusion quantifies over all x,y∈s and t∈[0,1]. No extra continuity of g, Hessian, measurable representative, integrability, domination or measure assumption is used.
Mathematical proof
1. Stay on one segment
Fix x,y in the domain, put d=y−x and N=‖d‖². Convexity of the domain keeps the full segment inside s. Subtract a scalar quadratic along that segment.
Corresponding Lean step
Local p and q select this segment; hp uses Convex.add_smul_sub_mem.
2. Compute the genuine derivative
Apply the chain rule to f composed with the affine segment, then differentiate the quadratic. The ambient gradient hypothesis supplies differentiability even at the endpoints. Therefore q is continuous on [0,1] and differentiable on its interior.
Corresponding Lean step
hq combines HasGradientAt.hasFDerivAt, HasFDerivAt.comp_hasDerivAt and derivatives of powers and scalar products.
3. Cancel only a positive scalar
For 0≤u<v≤1, the displacement is p(v)−p(u)=(v−u)d. Apply the gradient bound and divide by the positive parameter difference. Subtracting the quadratic derivative gives monotonicity of q′. Equal parameters require no division.
Corresponding Lean step
hdis rewrites the displacement. hscaled rewrites norm_smul using |v−u|²=(v−u)². le_of_mul_le_mul_left cancels v−u>0; hmon handles equality separately.
4. Use scalar convexity
The mean value theorem implies that a continuous scalar function with nondecreasing derivative is convex on the interval. All three hypotheses have been established, so the chord bound for q follows.
Corresponding Lean step
hconv applies Mathlib MonotoneOn.convexOn_of_deriv. hq.deriv identifies the library derivative with the supplied q′. hchord evaluates the resulting ConvexOn inequality at 0 and 1.
5. Restore the quadratic correction
Expand q at the three parameters and use a=1−b. The difference between b and b² is ab, producing exactly the strong-convexity correction. Nothing here requires m≥0.
Corresponding Lean step
hpoint identifies ax+by with p(b). norm_sub_rev aligns norm conventions; substitution of a=1−b and ring arithmetic finish the inequality.
Lean statement · strongConvexOn_of_gradient_inner_lower_bound
Convex ℝ s and supplied HasGradientAt on s, together with the quantitative gradient bound for every ordered pair of domain points, imply StrongConvexOn s m f. The inherited CompleteSpace assumption is explicit.
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_of_gradient_inner_lower_bound
{s : Set E} {f : E → ℝ} {m : ℝ} {grad : E → E}
(hs : Convex ℝ s)
(hgrad : ∀ z ∈ s, HasGradientAt f (grad z) z)
(hmono : ∀ x ∈ s, ∀ y ∈ s,
m * ‖y - x‖ ^ 2 ≤ inner ℝ (grad y - grad x) (y - x)) :
StrongConvexOn s m fLean proof · strongConvexOn_of_gradient_inner_lower_bound
One segment-local quadratic correction reduces the target to Mathlib scalar derivative monotonicity. Equal segment parameters are separated before positive cancellation. The final chord bound uses the exact m/2 normalization.
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_of_gradient_inner_lower_bound
{s : Set E} {f : E → ℝ} {m : ℝ} {grad : E → E}
(hs : Convex ℝ s)
(hgrad : ∀ z ∈ s, HasGradientAt f (grad z) z)
(hmono : ∀ x ∈ s, ∀ y ∈ s,
m * ‖y - x‖ ^ 2 ≤ inner ℝ (grad y - grad x) (y - x)) :
StrongConvexOn s m f := by
refine ⟨hs, ?_⟩
intro x hx y hy a b ha hb hab
let p : ℝ → E := fun t => x + t • (y - x)
let q : ℝ → ℝ := fun t => f (p t) - m / 2 * t ^ 2 * ‖y - x‖ ^ 2
let q' : ℝ → ℝ := fun t => inner ℝ (grad (p t)) (y - x) - m * t * ‖y - x‖ ^ 2
have hp : ∀ t ∈ Icc (0 : ℝ) 1, p t ∈ s := by
intro t ht
exact hs.add_smul_sub_mem hx hy ht
have hq : ∀ t ∈ Icc (0 : ℝ) 1, HasDerivAt q (q' t) t := by
intro t ht
have hline : HasDerivAt (fun u => f (p u))
(inner ℝ (grad (p t)) (y - x)) t := by
have hpderiv : HasDerivAt p (y - x) t := by
simpa [p] using ((hasDerivAt_id t).smul_const (y - x)).const_add x
convert! (hgrad (p t) (hp t ht)).hasFDerivAt.comp_hasDerivAt t hpderiv using 1
have hquad := (((hasDerivAt_id t).pow 2).const_mul (m / 2)).mul_const (‖y - x‖ ^ 2)
convert! hline.sub hquad using 1
simp only [q', id_eq]
ring
have hmon : MonotoneOn q' (Icc (0 : ℝ) 1) := by
intro u hu v hv huv
rcases eq_or_lt_of_le huv with rfl | huv
· exact le_rfl
have h := hmono (p u) (hp u hu) (p v) (hp v hv)
have hdis : p v - p u = (v - u) • (y - x) := by
simp only [p, add_sub_add_left_eq_sub, sub_smul]
rw [hdis, inner_smul_right, norm_smul, Real.norm_eq_abs, mul_pow, sq_abs] at h
have hscaled : (v - u) * (m * (v - u) * ‖y - x‖ ^ 2) ≤
(v - u) * inner ℝ (grad (p v) - grad (p u)) (y - x) := by
nlinarith [h]
have hbound := le_of_mul_le_mul_left hscaled (sub_pos.mpr huv)
rw [inner_sub_left] at hbound
dsimp [q']
linarith
have hconv : ConvexOn ℝ (Icc (0 : ℝ) 1) q := by
apply MonotoneOn.convexOn_of_deriv (convex_Icc (0 : ℝ) 1)
(fun t ht => (hq t ht).continuousAt.continuousWithinAt)
(fun t ht => (hq t (interior_subset ht)).differentiableAt.differentiableWithinAt)
intro u hu v hv huv
rw [(hq u (interior_subset hu)).deriv, (hq v (interior_subset hv)).deriv]
exact hmon (interior_subset hu) (interior_subset hv) huv
have hchord := hconv.2 (show (0 : ℝ) ∈ Icc 0 1 by norm_num)
(show (1 : ℝ) ∈ Icc 0 1 by norm_num) ha hb hab
have hpoint : a • x + b • y = p b := by
have ha' : a = 1 - b := by linarith
simp [p, ha', sub_smul, smul_sub]
abel
rw [hpoint]
simp only [smul_eq_mul, mul_zero, mul_one, zero_add] at hchord ⊢
norm_num [q, p] at hchord
rw [norm_sub_rev] at hchord
have ha' : a = 1 - b := by linarith
rw [ha'] at hchord ⊢
dsimp [p]
nlinarith [hchord]
end AutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexGradientConverseScope and omitted-condition boundaries
- This is an ASTIS-owned port of the pinned Optlib Lower_Strong_Convex statement with its domain-local supplied-gradient assumptions.
- The proof uses a scalar mean-value route. Chewi Proposition 1.6 proves its whole-space C¹ reverse implication by integration; this module does not reproduce that integral argument or certify the entire equivalence.
- No geometric transport, gradient-flow convergence or Hessian result follows merely from publishing this declaration.
Source and reuse
ASTIS parents called
Mathlib API called (external library)
- MonotoneOn.convexOn_of_deriv — continuous scalar functions with monotone derivative are convex, proved using the mean value theorem.
- Convex.add_smul_sub_mem; convex_Icc — segment membership and scalar-domain convexity.
- HasGradientAt.hasFDerivAt; HasFDerivAt.comp_hasDerivAt; hasDerivAt_id; HasDerivAt.smul_const, const_add, pow, const_mul, mul_const, sub — differentiation.
- inner_smul_right; inner_sub_left; norm_smul; sq_abs; le_of_mul_le_mul_left; norm_sub_rev — gradient monotonicity and exact normalization.
Mathematical sources
- Optlib Lower_Strong_Convex (Apache-2.0; Chenyi Li and Ziyu Wang) — Exact domain-local theorem statement provenance; the upstream proof chain is not imported.
- Mathlib scalar derivative criterion — Actual compiled mean-value-theorem dependency.
- Focused quantitative consumers — Sharp signed quadratic modulus and a midpoint bound on a closed domain.
Existing Optlib mathematics adapted to pinned Mathlib 4.33.0. This is a compatibility integration, not a claim of first formalization. The implementation uses a segment-local quadratic correction instead of importing Optlib’s global quadratic-shift dependency chain.
ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.