A quadratic lower model from strong convexity
AutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexFirstOrder.firstOrder_lower_bound_of_strongConvexOn · theorem · Teaching coverage
Statement
On a convex subset of a real Hilbert space, a strongly convex function lies above its tangent model by a quadratic correction, provided its genuine gradients exist at the domain points.
All objects and hypotheses
- Let E be a complete real inner-product space, s⊆E, f:E→ℝ, m∈ℝ and g:E→E. For x,y∈s, assume StrongConvexOn s m f and HasGradientAt f (g z) z for every z∈s.
- StrongConvexOn includes convexity of s and the chord inequality with the normalization m/2.
- HasGradientAt is an ambient derivative of f at each z∈s, including boundary points; it is not merely a derivative within s or a totalized gradient value.
- m is an arbitrary real number. No measure, integration or continuity of the gradient field is assumed. CompleteSpace is retained from the reused Hilbert-space API.
Mathematical proof
1. Restrict to an affine segment
Set v=y−x and p(t)=x+tv. The chord inequality gives
Corresponding Lean step
path is the affine segment; hpoint rewrites the convex combination. hsc.2 supplies the chord inequality.
2. Divide by a positive parameter
Rearrange and divide by t:
Corresponding Lean step
The existing Geometry.GeodesicConvexity.firstOrder_geodesicConvexity parent handles the positive-parameter rearrangement; ASTIS does not duplicate that proof.
3. Take the one-sided limit
The genuine gradient identifies the difference-quotient limit below. Pass to the limit in the preceding inequality; the existing ASTIS firstOrder_geodesicConvexity theorem packages this scalar limiting step.
Corresponding Lean step
hline and hderiv obtain the real segment derivative from HasGradientAt; hfirst applies the scalar limit theorem and simpa reconciles norm and distance.
Lean statement · firstOrder_lower_bound_of_strongConvexOn
StrongConvexOn includes convexity of s and the chord inequality with the normalization m/2. HasGradientAt is an ambient derivative of f at each z∈s, including boundary points; it is not merely a derivative within s or a totalized gradient value. m is an arbitrary real number. No measure, integration or continuity of the gradient field is assumed. CompleteSpace is retained from the reused Hilbert-space API.
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 firstOrder_lower_bound_of_strongConvexOn
{s : Set E} {f : E → ℝ} {m : ℝ} {grad : E → E}
(hsc : StrongConvexOn s m f)
(hgrad : ∀ z ∈ s, HasGradientAt f (grad z) z)
{x y : E} (hx : x ∈ s) (hy : y ∈ s) :
f y ≥ f x + inner ℝ (grad x) (y - x) + m / 2 * ‖y - x‖ ^ 2Lean proof · firstOrder_lower_bound_of_strongConvexOn
The local definitions path and isSelected encode the chosen affine segment; hconvex rewrites the Mathlib chord inequality into the geodesic parent's normalization. hgrad supplies HasFDerivAt, then HasLineDerivAt; hderiv identifies the real derivative of the segment composition. simpa reconciles dist and norm conventions.
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 firstOrder_lower_bound_of_strongConvexOn
{s : Set E} {f : E → ℝ} {m : ℝ} {grad : E → E}
(hsc : StrongConvexOn s m f)
(hgrad : ∀ z ∈ s, HasGradientAt f (grad z) z)
{x y : E} (hx : x ∈ s) (hy : y ∈ s) :
f y ≥ f x + inner ℝ (grad x) (y - x) + m / 2 * ‖y - x‖ ^ 2 := by
let path : ℝ → E := fun t => x + t • (y - x)
let isSelected : (ℝ → E) → Prop := fun q => q = path
have hpath : isSelected path := rfl
have hconvex :
Geometry.GeodesicConvexity.IsAlphaGeodesicallyConvex isSelected f m := by
intro q hq t ht
subst q
have hnonneg_left : 0 ≤ 1 - t := sub_nonneg.mpr ht.2
have hnonneg_right : 0 ≤ t := ht.1
have hstrong := hsc.2 hx hy hnonneg_left hnonneg_right (by ring)
have hpoint : path t = (1 - t) • x + t • y := by
dsimp only [path]
rw [smul_sub, sub_smul, one_smul]
abel
calc
f (path t) = f ((1 - t) • x + t • y) := congrArg f hpoint
_ ≤ (1 - t) * f x + t * f y -
(1 - t) * t * (m / 2 * ‖x - y‖ ^ 2) := by
simpa [smul_eq_mul] using hstrong
_ = (1 - t) * f (path 0) + t * f (path 1) -
(m * t * (1 - t) / 2) * dist (path 0) (path 1) ^ 2 := by
simp [path, dist_eq_norm]
ring
have hline :
HasLineDerivAt ℝ f (inner ℝ (grad x) (y - x)) x (y - x) := by
have h := (hgrad x hx).hasFDerivAt.hasLineDerivAt (y - x)
simpa [InnerProductSpace.toDual_apply_apply] using h
have hderiv :
HasDerivAt (fun t : ℝ => f (path t)) (inner ℝ (grad x) (y - x)) 0 := by
simpa [HasLineDerivAt, path] using hline
have hfirst :=
Geometry.GeodesicConvexity.firstOrder_geodesicConvexity
hconvex hpath hderiv
simpa [path, dist_eq_norm, norm_sub_rev] using hfirst
/-- The gradient of a strongly convex function has the corresponding inner-product
lower bound on its domain.
Mathematical provenance: Optlib `Strong_Convex_lower`, commit
`5da27c5f95aa6a8a45b8c14b968ade4c13ff18c3`,
`Optlib/Convex/StronglyConvex.lean` (Apache-2.0; Chenyi Li and Ziyu Wang).
This proof reuses the local first-order bound in both directions, as in Chewi,
arXiv:2605.07006v1, Proposition 1.6, (1.4) implies (1.5).
The domain-local supplied-gradient interface retains arbitrary real `m`;
Chewi's whole-space `C¹`, nonnegative-modulus statement is a specialization.
-/Scope and omitted-condition boundaries
- Convexity keeps the segment in the domain; positive t permits division without reversing the inequality.
- Genuine differentiability identifies the difference-quotient limit. The domain-local interface is not a claim that Chewi's entire whole-space C¹ equivalence is formalized.
- Existing parent from PR #239, newly registered during PR #248 integration, not a newly proved result.
Source and reuse
ASTIS parents called
Mathlib API called (external library)
- StrongConvexOn — convex domain and m/2 normalization.
- HasGradientAt.hasFDerivAt; HasFDerivAt.hasLineDerivAt; HasLineDerivAt — genuine derivative interfaces.
- InnerProductSpace.toDual_apply_apply; dist_eq_norm; norm_sub_rev — gradient, distance and norm identifications.
Mathematical sources
- Optlib, Chenyi Li and Ziyu Wang (Apache-2.0), pinned source — Strong_Convex_second_lower: mathematical statement provenance; ASTIS uses its existing geodesic limiting proof.
- Sinho Chewi, Lectures on Optimization, §1.2, Proposition 1.6 — (1.3) implies (1.4). Domain-local supplied gradients are explicit in the ASTIS interface, not silently attributed to the source.
- Exact focused tests — Uses the first-order bound and checks positive-modulus gradient injectivity.
Mathematical statement provenance: Optlib Strong_Convex_second_lower, commit 5da27c5f95aa6a8a45b8c14b968ade4c13ff18c3 (Chenyi Li and Ziyu Wang, Apache-2.0). ASTIS reuses its own geodesic limiting proof, not an imported Optlib proof. Chewi Lectures on Optimization, arXiv:2605.07006v1, Proposition 1.6, (1.3)→(1.4), is the whole-space specialization.
ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.