theorem ConvexC1SeminormSmooth.gradient_pairing_with_minimizer_gap_ge_norm_sq_div {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {L : NNReal} {f : E → ℝ} (hconv : ConvexOn ℝ Set.univ f) (hgrad : ∀ (x : E), HasGradientAt f (gradient f x) x) (hgrad_lipschitz : LipschitzWith L (gradient f)) {xStar : E} (hxStar : IsMinOn f Set.univ xStar) (x : E) : 1 / ↑L * ‖gradient f x‖ ^ 2 ≤ inner ℝ (gradient f x) (x - xStar)

Lemma 2.17 on the intrinsic real-Hilbert-space smooth-convex owner layer: if f is convex on the whole space, admits the ambient gradient ∇ f everywhere, has L-Lipschitz gradient, and xStar is a global minimizer, then every point x satisfies (1 / L) ‖∇ f x‖² ≤ ⟪∇ f x, x - xStar⟫. The textbook ℝⁿ statement is recovered by the finite-dimensional specialization theorem below.

theorem ConvexC1SeminormSmooth.lemma17FiniteDimensionalComplete {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] : CompleteSpace E

theorem ConvexC1SeminormSmooth.gradient_pairing_with_minimizer_gap_ge_norm_sq_div_of_mem_F11 {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {L : NNReal} {f : E → ℝ} (hf : f ∈ setOf (ConvexC1SeminormSmooth (normSeminorm ℝ E) L)) {xStar : E} (hxStar : IsMinOn f Set.univ xStar) (x : E) : 1 / ↑L * ‖gradient f x‖ ^ 2 ≤ inner ℝ (gradient f x) (x - xStar)

Finite-dimensional Chapter 2 specialization of Lemma 2.17: the source-facing notation f ∈ 𝓕[L, normSeminorm ℝ E]¹¹ supplies the intrinsic owner hypotheses used by gradient_pairing_with_minimizer_gap_ge_norm_sq_div.