Samplinglib mathematical lesson

Strong convexity separates gradients

AutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexFirstOrder.gradient_inner_lower_bound_of_strongConvexOn · theorem · Teaching coverage

Read this first

Mathematical statement

The gradient of a strongly convex function has a quantitative monotonicity bound on its domain. A positive modulus therefore makes the gradient injective there.

\[\langle g(y)-g(x),y-x\rangle\ge m\|y-x\|^2.\]

Lean statement · gradient_inner_lower_bound_of_strongConvexOn

The set is convex as part of StrongConvexOn. Both x and y belong to s. Supplied gradients are genuine ambient derivatives at all domain points; no totalized derivative is used to manufacture differentiability. Complete real inner-product space, with arbitrary real m. No extra smoothness, Hessian, measure or integrability assumptions.

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.

Download module (.lean)

theorem gradient_inner_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) :
    m * ‖y - x‖ ^ 2 ≤ inner ℝ (grad y - grad x) (y - x)

Exact module and namespace context

Proof roadmap

1The lower model at x
Put v=y−x. Apply the parent at (x,y):
2The lower model at y
Apply the same parent at (y,x), using x−y=−v:
3Cancel and collect
Add, cancel the function values, and use linearity of the real inner product. Rearranging the following inequality proves the claimed bound.
4The positive-modulus test consumer
If m>0 and g(x)=g(y), the bound forces the displacement to vanish, as calculated below. The focused test checks this consequence; it is not a second registered theorem.

Full assumptions and notation

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.
The set is convex as part of StrongConvexOn. Both x and y belong to s.
Supplied gradients are genuine ambient derivatives at all domain points; no totalized derivative is used to manufacture differentiability.
Complete real inner-product space, with arbitrary real m. No extra smoothness, Hessian, measure or integrability assumptions.

Mathematical proof

1. The lower model at x

Put v=y−x. Apply the parent at (x,y):

\[f(y)-f(x)\ge\langle g(x),v\rangle+\frac m2\|v\|^2.\]

Corresponding Lean step

hxy applies the existing first-order bound with hx hy.

2. The lower model at y

Apply the same parent at (y,x), using x−y=−v:

\[f(x)-f(y)\ge-\langle g(y),v\rangle+\frac m2\|v\|^2.\]

Corresponding Lean step

hyx applies that same bound with hy hx. Rewriting uses the reversed-displacement identity, inner_neg_right and norm_neg.

3. Cancel and collect

Add, cancel the function values, and use linearity of the real inner product. Rearranging the following inequality proves the claimed bound.

\[0\ge-\langle g(y)-g(x),v\rangle+m\|v\|^2.\]

Corresponding Lean step

rw [inner_sub_left] expands the goal. linarith combines the two inequalities and cancels the function values.

4. The positive-modulus test consumer

If m>0 and g(x)=g(y), the bound forces the displacement to vanish, as calculated below. The focused test checks this consequence; it is not a second registered theorem.

\[0\ge m\|y-x\|^2\ge0\quad\Longrightarrow\quad x=y.\]

Corresponding Lean step

The Set.InjOn example substitutes equal gradients. mul_pos hm (pow_pos hn' 2) excludes a nonzero displacement, and norm_eq_zero and sub_eq_zero conclude equality.

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · gradient_inner_lower_bound_of_strongConvexOn

hxy and hyx are the two calls to the same ASTIS parent. rw changes the reversed displacement to a negative, normalizes its norm, and expands inner_sub_left. linarith combines the two scalar inequalities without assuming the desired conclusion.

Download module (.lean)

theorem gradient_inner_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) :
    m * ‖y - x‖ ^ 2 ≤ inner ℝ (grad y - grad x) (y - x) := by
  have hxy := firstOrder_lower_bound_of_strongConvexOn hsc hgrad hx hy
  have hyx := firstOrder_lower_bound_of_strongConvexOn hsc hgrad hy hx
  rw [show x - y = -(y - x) by abel, inner_neg_right, norm_neg] at hyx
  rw [inner_sub_left]
  linarith

end

end StrongConvexFirstOrder
end Analysis
end TechnicalLemmas
end AutoSamplingTheory

Exact module and namespace context

Scope and omitted-condition boundaries

The existing first-order bound is used at both endpoints. The proof adds no assumptions beyond that parent interface.
The lower bound is strong monotonicity only when m>0, ordinary monotonicity when m=0, and a signed lower bound when m<0.
No reverse implication, Hessian equivalence, gradient-flow contraction, Gibbs invariance or sampling rate is proved. The injectivity test is not another registered leaf.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

AutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexFirstOrder.firstOrder_lower_bound_of_strongConvexOn

Mathlib API called (external library)

inner_neg_right; norm_neg; inner_sub_left — inner-product and norm identities.
abel; linarith — checked algebraic normalization and linear arithmetic.

Mathematical sources

Optlib, Chenyi Li and Ziyu Wang (Apache-2.0), pinned source — Strong_Convex_lower: matching domain-local statement after swapping x and y; ASTIS uses its own first-order parent rather than this external proof code.
Sinho Chewi, Lectures on Optimization, §1.2, Proposition 1.6 — (1.4) implies (1.5). The whole-space C¹, nonnegative-modulus formulation is a specialization; the full equivalence remains open.
Exact focused tests — Uses the first-order bound and checks positive-modulus gradient injectivity.

Source correspondence: Chewi Lectures on Optimization, arXiv:2605.07006v1, Proposition 1.6, (1.4)→(1.5). Reverse implications, Hessian equivalence, whole-space source-facing specialization and gradient-flow contraction remain separate obligations. This is not a Gibbs-invariance or sampling-rate theorem.

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