LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Strong convexity makes a differentiable gradient strongly monotone

Statement

Let $U \subseteq R^{d}$ be open and convex, let $C \subseteq U$ be convex, and let $f : U \to R$ be differentiable. Suppose $f ∣_{C}$ is $μ$ -strongly convex in the strong-Jensen sense of Strong convexity for an extended-real objective, for $μ > 0$ ; explicitly, for $x, y \in C$ and $0 < t < 1$ , $f ((1 - t) x + t y) \leq (1 - t) f (x) + t f (y) - \frac{μ}{2} t (1 - t) ∥ x - y ∥_{2}^{2} .$ Then for all $x, y \in C$ , $f (y) \geq f (x) + ⟨ \nabla f (x), y - x ⟩ + \frac{μ}{2} ∥ y - x ∥_{2}^{2},$ and consequently $⟨ \nabla f (x) - \nabla f (y), x - y ⟩ \geq μ ∥ x - y ∥_{2}^{2} .$

Facts & Assumptions

Given: $U, C, f, μ$ and the strong-convexity hypothesis in the Statement.

[F1]

Strong convexity for an extended-real objective: for $x, y \in dom F$ and $0 < t < 1$ , $F ((1 - t) x + t y) \leq (1 - t) F (x) + t F (y) - (μ / 2) t (1 - t) ∥ x - y ∥_{2}^{2}$ .

[F2]

The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ : along the segment $s \mapsto x + s (y - x)$ , the derivative of $f$ is $⟨ \nabla f (x + s (y - x)), y - x ⟩$ .

[F3]

The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ : the real Euclidean inner product is symmetric and $∥ v ∥_{2}^{2} = ⟨ v, v ⟩$ .

Proof

1.1F1givenalgebra

Fix $x, y \in C$ , put $d = y - x$ , and take $0 < t < 1$ . Since $F = f$ on $C$ , [F1] gives $\frac{f (x + t d) - f (x)}{t} \leq f (y) - f (x) - \frac{μ}{2} (1 - t) ∥ d ∥_{2}^{2} .$

2.1F2step 1.1algebra

As $t ↓ 0$ , [F2] makes the left side tend to $⟨ \nabla f (x), d ⟩$ ; the right side tends to $f (y) - f (x) - (μ / 2) ∥ d ∥_{2}^{2}$ . The inequality persists in the limit: if the left limit exceeded the right limit, their difference would stay positive for sufficiently small $t$ , contradicting step 1.1. Thus the first displayed conclusion follows.

3.1F3step 2.1algebra∎

Apply step 2.1 once to $(x, y)$ and once to $(y, x)$ , then add. The function-value terms cancel and symmetry in [F3] gives $⟨ \nabla f (x) - \nabla f (y), x - y ⟩ \geq μ ∥ x - y ∥_{2}^{2}$ , proving the second conclusion.

Depends on

Used by

Dependency tree · two levels

22 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Sébastien Bubeck, Convex Optimization: Algorithms and Complexity, §3.4.2 (standard reference, not scraped)
Léon Bottou, Frank E. Curtis, and Jorge Nocedal, Optimization Methods for Large-Scale Machine Learning, SIAM Review 60(2) (2018), §4.2 (standard reference, not scraped)