theorem abs_sub_sub_inner_gradientWithin_le_half_mul {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {U : Set H} {β : NNReal} {f : H → ℝ} (hU_open : IsOpen U) (hU_convex : Convex ℝ U) (hf : DifferentiableOn ℝ f U) (hgrad : LipschitzOnWith β (gradientWithin f U) U) {x y : H} (hx : x ∈ U) (hy : y ∈ U) : |f y - f x - inner ℝ (y - x) (gradientWithin f U x)| ≤ ↑β / 2 * ‖y - x‖ ^ 2

Lemma 2.64 (1): on an open convex set, a Fréchet differentiable function whose gradient is β-Lipschitz has first-order Taylor remainder at most (β / 2) * ‖y - x‖^2.

theorem abs_inner_sub_gradientWithin_sub_le_mul {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {U : Set H} {β : NNReal} {f : H → ℝ} (hgrad : LipschitzOnWith β (gradientWithin f U) U) {x y : H} (hx : x ∈ U) (hy : y ∈ U) : |inner ℝ (x - y) (gradientWithin f U x - gradientWithin f U y)| ≤ ↑β * ‖y - x‖ ^ 2

Lemma 2.64 (2): for points of U, the gradient increment paired with x - y is bounded in absolute value by β * ‖y - x‖^2.