feat(LipschitzSmooth): algebraic preservation lemmas

Mathlib/Analysis/Calculus/LipschitzSmooth/Algebra.lean

@@ -0,0 +1,97 @@
+/-
+Copyright (c) 2026 Christoph Spiegel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christoph Spiegel
+-/
+module
+
+public import Mathlib.Analysis.Calculus.LipschitzSmooth.FDeriv
+public import Mathlib.Analysis.Normed.Affine.ContinuousAffineMap
+
+/-!
+# Algebraic preservation of Lipschitz smoothness
+
+Closure properties of the `LipschitzSmoothWith` predicate under the standard algebraic
+operations: pointwise addition (with `K₁ + K₂`), nonnegative scalar multiplication (with
+`c · K`), and composition with continuous affine maps (with `‖A.contLinear‖² · K`). The
+two-sided abs-form of the predicate also makes it closed under negation (same `K`) and so
+under scaling by arbitrary real `c` (with `|c| · K`).
+
+The basic K = 0 cases for constants and affine functions live in
+`Mathlib.Analysis.Calculus.LipschitzSmooth.Basic`. None of the lemmas here require any
+differentiability hypothesis — `LipschitzSmoothWith` implies line-differentiability
+everywhere via `LipschitzSmoothWith.hasLineDerivAt`.
+-/
+
+public section
+
+variable {F F' : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
+  [NormedAddCommGroup F'] [NormedSpace ℝ F']
+variable {K K₁ K₂ : NNReal} {f f₁ f₂ : F → ℝ}
+
+/-- A continuous affine map `A : F →ᴬ[ℝ] ℝ` is `0`-smooth. Bundled form of
+`lipschitzSmoothWith_affine` (which splits into linear part + constant). -/
+theorem lipschitzSmoothWith_continuousAffineMap (A : F →ᴬ[ℝ] ℝ) :
+    LipschitzSmoothWith (0 : NNReal) (A : F → ℝ) := by
+  rw [show (A : F → ℝ) = ⇑A.contLinear + Function.const F (A 0) from A.decomp]
+  exact lipschitzSmoothWith_affine A.contLinear (A 0)
+
+namespace LipschitzSmoothWith
+
+/-- Sum of `K₁`-smooth and `K₂`-smooth is `(K₁ + K₂)`-smooth. No differentiability hypothesis
+needed: each summand is line-differentiable everywhere (`hasLineDerivAt`), so the sum is too,
+with line-derivative the sum of line-derivatives. -/
+theorem add (h₁ : LipschitzSmoothWith K₁ f₁) (h₂ : LipschitzSmoothWith K₂ f₂) :
+    LipschitzSmoothWith (K₁ + K₂) (f₁ + f₂) := lipschitzSmoothWith_iff_lineDeriv.mpr fun x y => by
+  have hd : HasLineDerivAt ℝ (f₁ + f₂)
+      (lineDeriv ℝ f₁ x (y - x) + lineDeriv ℝ f₂ x (y - x)) x (y - x) :=
+    HasDerivAt.add (h₁.hasLineDerivAt x (y - x)) (h₂.hasLineDerivAt x (y - x))
+  rw [hd.lineDeriv]
+  have h1 := h₁.lineDeriv_abs_le x y
+  have h2 := h₂.lineDeriv_abs_le x y
+  calc |(f₁ + f₂) y - (f₁ + f₂) x - (lineDeriv ℝ f₁ x (y - x) + lineDeriv ℝ f₂ x (y - x))|
+      = |(f₁ y - f₁ x - lineDeriv ℝ f₁ x (y - x))
+          + (f₂ y - f₂ x - lineDeriv ℝ f₂ x (y - x))| := by
+        simp only [Pi.add_apply]; ring_nf
+    _ ≤ |f₁ y - f₁ x - lineDeriv ℝ f₁ x (y - x)|
+        + |f₂ y - f₂ x - lineDeriv ℝ f₂ x (y - x)| := abs_add_le _ _
+    _ ≤ ↑(K₁ + K₂) / 2 * (dist x y) ^ 2 := by push_cast; linarith
+
+/-- Negation preserves `K`-smoothness with the same constant. Trivial under the two-sided
+abs form of the predicate. -/
+theorem neg (h : LipschitzSmoothWith K f) : LipschitzSmoothWith K (-f) :=
+    lipschitzSmoothWith_iff_lineDeriv.mpr fun x y => by
+  have hd : HasLineDerivAt ℝ (-f) (-lineDeriv ℝ f x (y - x)) x (y - x) :=
+    HasDerivAt.neg (h.hasLineDerivAt x (y - x))
+  rw [hd.lineDeriv]
+  have habs := h.lineDeriv_abs_le x y
+  rw [show ((-f) y - (-f) x - -lineDeriv ℝ f x (y - x))
+      = -(f y - f x - lineDeriv ℝ f x (y - x)) from by simp; ring, abs_neg]
+  exact habs
+
+/-- Scaling a `K`-smooth function by `c : NNReal` gives `(c * K)`-smoothness. No
+differentiability hypothesis needed: line-differentiability follows from `hasLineDerivAt`. -/
+theorem const_smul (h : LipschitzSmoothWith K f) (c : NNReal) :
+    LipschitzSmoothWith (c * K) ((c : ℝ) • f) := lipschitzSmoothWith_iff_lineDeriv.mpr fun x y => by
+  have hd : HasLineDerivAt ℝ ((c : ℝ) • f) ((c : ℝ) • lineDeriv ℝ f x (y - x)) x (y - x) :=
+    (h.hasLineDerivAt x (y - x)).const_smul (c : ℝ)
+  rw [hd.lineDeriv]
+  have habs := h.lineDeriv_abs_le x y
+  have hc : (0 : ℝ) ≤ c := c.coe_nonneg
+  calc |((c : ℝ) • f) y - ((c : ℝ) • f) x - (c : ℝ) • lineDeriv ℝ f x (y - x)|
+      = (c : ℝ) * |f y - f x - lineDeriv ℝ f x (y - x)| := by
+        simp only [Pi.smul_apply, smul_eq_mul]
+        rw [show (c : ℝ) * f y - (c : ℝ) * f x - (c : ℝ) * lineDeriv ℝ f x (y - x)
+            = (c : ℝ) * (f y - f x - lineDeriv ℝ f x (y - x)) from by ring,
+          abs_mul, abs_of_nonneg hc]
+    _ ≤ ↑(c * K) / 2 * (dist x y) ^ 2 := by
+        push_cast
+        nlinarith [sq_nonneg (dist x y), K.coe_nonneg]
+
+/-- Composition of a `K`-smooth `f : F → ℝ` with a continuous affine map `A : F' →ᴬ[ℝ] F`
+is `(‖A.contLinear‖² · K)`-smooth on `F'`. -/
+theorem comp_continuousAffineMap (h : LipschitzSmoothWith K f) (A : F' →ᴬ[ℝ] F) :
+    LipschitzSmoothWith (‖A.contLinear‖₊ ^ 2 * K) (f ∘ A) :=
+  sorry
+
+end LipschitzSmoothWith

Mathlib/Analysis/Calculus/LipschitzSmooth/Basic.lean

@@ -10,49 +10,129 @@ public import Mathlib.Analysis.Calculus.LineDeriv.Basic
 /-!
 # Lipschitz smoothness
 
-A real-valued function `f` on a normed real vector space is **`K`-smooth** if it satisfies
-the quadratic descent inequality
+A real-valued function `f` on a normed real vector space is **`K`-smooth** if the
+first-order Taylor remainder is bounded quadratically:
 
-`f y ≤ f x + lineDeriv ℝ f x (y - x) + (K / 2) (dist x y)²`
+`|f y - f x - lineDeriv ℝ f x (y - x)| ≤ (K / 2) (dist x y)²`
 
 for all `x, y`. The predicate uses `lineDeriv` so as not to presuppose Fréchet
-differentiability; restatements in `fderiv`, 1D `deriv`, and Hilbert-space gradient
-form live in the sibling files in this directory.
+differentiability; equivalent characterisations in `fderiv`, 1D `deriv`, and
+Hilbert-space gradient form live in the sibling files in this directory.
+
+This two-sided (absolute-value) form is orientation-agnostic (closed under
+`f ↦ -f`) — matching the textbook notion of L-smoothness (Lipschitz gradient,
+the class `C^{1,1}`) used in Nesterov, Beck, Bauschke-Combettes, etc.
 -/
 
 public section
 
 variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
 
 /-- A real-valued function `f` on a normed real vector space `F` is `K`-smooth
-if it satisfies the quadratic descent inequality
-`f y ≤ f x + lineDeriv ℝ f x (y - x) + (K / 2) (dist x y)²` for all `x, y`.
+if the first-order Taylor remainder is bounded quadratically:
+`|f y - f x - lineDeriv ℝ f x (y - x)| ≤ (K / 2) (dist x y)²` for all `x, y`.
+
+The predicate is two-sided (absolute value), so closed under `f ↦ -f` and
+matching the textbook L-smoothness / `C^{1,1}` class. The `lineDeriv` form is
+the weakest possible underlying derivative form — the predicate implies
+line-differentiability everywhere (`LipschitzSmoothWith.hasLineDerivAt`), so
+the `lineDeriv` value is always the actual line derivative.
 
-The choice of `lineDeriv` here is an implementation detail: it is the weakest form
-that makes the predicate well-defined for non-differentiable functions. Equivalent
-characterisations in `fderiv`, `gradient`, and `deriv` form are provided in the
-sibling files, predicated on the appropriate differentiability hypothesis. -/
+Equivalent characterisations in `fderiv`, `gradient`, and `deriv` form are
+provided in the sibling files, predicated on `Differentiable` where useful. -/
 def LipschitzSmoothWith (K : NNReal) (f : F → ℝ) :=
-  ∀ (x y : F), f y ≤ f x + lineDeriv ℝ f x (y - x) + ↑K / 2 * (dist x y) ^ 2
+  ∀ (x y : F), |f y - f x - lineDeriv ℝ f x (y - x)| ≤ ↑K / 2 * (dist x y) ^ 2
 
 theorem lipschitzSmoothWith_iff_lineDeriv {K : NNReal} {f : F → ℝ} : LipschitzSmoothWith K f ↔
-    ∀ x y : F, f y ≤ f x + lineDeriv ℝ f x (y - x) + ↑K / 2 * (dist x y) ^ 2 := Iff.rfl
+    ∀ x y : F, |f y - f x - lineDeriv ℝ f x (y - x)| ≤ ↑K / 2 * (dist x y) ^ 2 := Iff.rfl
 
 namespace LipschitzSmoothWith
 
 variable {K : NNReal} {f : F → ℝ}
 
+/-- Primary extractor: the Taylor remainder is bounded in absolute value. -/
+theorem lineDeriv_abs_le (h : LipschitzSmoothWith K f) (x y : F) :
+    |f y - f x - lineDeriv ℝ f x (y - x)| ≤ ↑K / 2 * (dist x y) ^ 2 := h x y
+
+/-- Descent inequality (upper-bound extractor). -/
 theorem lineDeriv_descent_le (h : LipschitzSmoothWith K f) (x y : F) :
-    f y ≤ f x + lineDeriv ℝ f x (y - x) + ↑K / 2 * (dist x y) ^ 2 := h x y
+    f y ≤ f x + lineDeriv ℝ f x (y - x) + ↑K / 2 * (dist x y) ^ 2 := by
+  have := (abs_le.mp (h.lineDeriv_abs_le x y)).2
+  linarith
 
+/-- Ascent inequality (lower-bound extractor). -/
+theorem lineDeriv_descent_ge (h : LipschitzSmoothWith K f) (x y : F) :
+    f x + lineDeriv ℝ f x (y - x) - ↑K / 2 * (dist x y) ^ 2 ≤ f y := by
+  have := (abs_le.mp (h.lineDeriv_abs_le x y)).1
+  linarith
+
+/-- One-sided variance bound on the line derivative. -/
 theorem lineDeriv_apply_sub_le (h : LipschitzSmoothWith K f) (x y : F) :
     lineDeriv ℝ f y (y - x) - lineDeriv ℝ f x (y - x) ≤ ↑K * (dist x y) ^ 2 := by
   have hyx := h.lineDeriv_descent_le y x
   rw [← neg_sub y x, lineDeriv_neg, dist_comm] at hyx
   linarith [h.lineDeriv_descent_le x y, hyx]
 
+/-- Two-sided variance bound on the line derivative. -/
+theorem lineDeriv_apply_sub_abs_le (h : LipschitzSmoothWith K f) (x y : F) :
+    |lineDeriv ℝ f y (y - x) - lineDeriv ℝ f x (y - x)| ≤ ↑K * (dist x y) ^ 2 := by
+  rw [abs_le]
+  refine ⟨?_, h.lineDeriv_apply_sub_le x y⟩
+  have hyx := h.lineDeriv_descent_ge y x
+  rw [← neg_sub y x, lineDeriv_neg, dist_comm] at hyx
+  linarith [h.lineDeriv_descent_ge x y]
+
+/-- Functional-form variance bound. -/
 theorem lineDeriv_sub_apply_le (h : LipschitzSmoothWith K f) (x y : F) :
     (lineDeriv ℝ f y - lineDeriv ℝ f x) (y - x) ≤ ↑K * (dist x y) ^ 2 :=
   Pi.sub_apply (lineDeriv ℝ f _) _ _ ▸ h.lineDeriv_apply_sub_le x y
 
+/-- `K`-smoothness implies line-differentiability: the actual line derivative
+exists at every `x, v` and equals `lineDeriv ℝ f x v`. The predicate bound
+`|f(x + tv) - f x - t · L| ≤ K/2 · t² ‖v‖²` (via `lineDeriv_smul` to factor `t`)
+is `o(t)`. -/
+theorem hasLineDerivAt (h : LipschitzSmoothWith K f) (x v : F) :
+    HasLineDerivAt ℝ f (lineDeriv ℝ f x v) x v := by
+  set L := lineDeriv ℝ f x v
+  change HasDerivAt (fun t : ℝ => f (x + t • v)) L 0
+  rw [hasDerivAt_iff_isLittleO_nhds_zero, Asymptotics.isLittleO_iff]
+  intro ε hε
+  have hsum_pos : (0:ℝ) < ↑K * ‖v‖^2 / 2 + 1 := by positivity
+  filter_upwards [Metric.ball_mem_nhds (0 : ℝ) (div_pos hε hsum_pos)] with t ht
+  simp only [Metric.mem_ball, Real.dist_eq, sub_zero] at ht
+  simp only [zero_add, zero_smul, add_zero, smul_eq_mul, Real.norm_eq_abs]
+  have hpred := h x (x + t • v)
+  rw [show (x + t • v) - x = t • v from by abel, lineDeriv_smul, smul_eq_mul,
+      dist_self_add_right, norm_smul, Real.norm_eq_abs, mul_pow, sq_abs] at hpred
+  refine hpred.trans ?_
+  have ht' : |t| * (↑K * ‖v‖^2 / 2 + 1) < ε := (lt_div_iff₀ hsum_pos).mp ht
+  have ht'' : ↑K * ‖v‖^2 / 2 * |t| ≤ ε := by nlinarith [abs_nonneg t]
+  calc ↑K / 2 * (t ^ 2 * ‖v‖ ^ 2)
+      = ↑K * ‖v‖^2 / 2 * |t| * |t| := by rw [← sq_abs t]; ring
+    _ ≤ ε * |t| := mul_le_mul_of_nonneg_right ht'' (abs_nonneg t)
+
+/-- A `K`-smooth function is line-differentiable everywhere. -/
+theorem lineDifferentiableAt (h : LipschitzSmoothWith K f) (x v : F) :
+    LineDifferentiableAt ℝ f x v :=
+  (h.hasLineDerivAt x v).lineDifferentiableAt
+
+/-- A `K`-smooth function is continuous. -/
+theorem continuous (h : LipschitzSmoothWith K f) : Continuous f :=
+  sorry
+
 end LipschitzSmoothWith
+
+/-! ### Algebraic preservation -/
+
+/-- An affine function `y ↦ ℓ y + c` is `0`-smooth. -/
+theorem lipschitzSmoothWith_affine (ℓ : F →L[ℝ] ℝ) (c : ℝ) :
+    LipschitzSmoothWith (0 : NNReal) (fun y => ℓ y + c) :=
+  lipschitzSmoothWith_iff_lineDeriv.mpr fun x y => by
+    have h : HasFDerivAt (fun y : F => ℓ y + c) ℓ x := ℓ.hasFDerivAt.add_const c
+    rw [(h.hasLineDerivAt (y - x)).lineDeriv, map_sub]
+    simp
+
+/-- A constant function is `0`-smooth. Special case of `lipschitzSmoothWith_affine` with `ℓ = 0`. -/
+theorem lipschitzSmoothWith_const (c : ℝ) : LipschitzSmoothWith (0 : NNReal) (fun _ : F => c) := by
+  simpa using lipschitzSmoothWith_affine (0 : F →L[ℝ] ℝ) c
+

Mathlib/Analysis/Calculus/LipschitzSmooth/Deriv.lean

@@ -11,11 +11,11 @@ public import Mathlib.Analysis.Calculus.LipschitzSmooth.FDeriv
 /-!
 # Lipschitz smoothness in 1D via the derivative
 
-For a `K`-smooth function `f : ℝ → ℝ`, the descent inequality and the variation bound
-take their classical 1D forms
+For a `K`-smooth function `f : ℝ → ℝ`, the Taylor bound and the variation bound take
+their classical 1D forms:
 
-`f y ≤ f x + deriv f x * (y - x) + K/2 * (y - x)²`,
-`(deriv f y - deriv f x) * (y - x) ≤ K * (y - x)²`.
+`|f y - f x - deriv f x · (y - x)| ≤ K/2 · (y - x)²`,
+`(deriv f y - deriv f x) · (y - x) ≤ K · (y - x)²`.
 
 These are 1D restatements of the Fréchet-derivative forms in
 `Mathlib.Analysis.Calculus.LipschitzSmooth.FDeriv`, lifted via `fderiv_eq_deriv_mul`.
@@ -26,18 +26,28 @@ public section
 variable {K : NNReal} {f : ℝ → ℝ}
 
 theorem lipschitzSmoothWith_iff_deriv (hf : Differentiable ℝ f) : LipschitzSmoothWith K f ↔
-    ∀ x y : ℝ, f y ≤ f x + deriv f x * (y - x) + ↑K / 2 * (y - x) ^ 2 := by
+    ∀ x y : ℝ, |f y - f x - deriv f x * (y - x)| ≤ ↑K / 2 * (y - x) ^ 2 := by
   rw [lipschitzSmoothWith_iff_fderiv hf]
   refine forall_congr' fun x => forall_congr' fun y => ?_
   rw [fderiv_eq_deriv_mul, dist_comm, Real.dist_eq, sq_abs]
 
 namespace LipschitzSmoothWith
 
+theorem deriv_abs_le (h : LipschitzSmoothWith K f) (x y : ℝ) (hf : DifferentiableAt ℝ f x) :
+    |f y - f x - deriv f x * (y - x)| ≤ ↑K / 2 * (y - x) ^ 2 := by
+  have := h.fderiv_abs_le x y hf
+  rwa [fderiv_eq_deriv_mul, dist_comm, Real.dist_eq, sq_abs] at this
+
 theorem deriv_descent_le (h : LipschitzSmoothWith K f) (x y : ℝ) (hf : DifferentiableAt ℝ f x) :
     f y ≤ f x + deriv f x * (y - x) + ↑K / 2 * (y - x) ^ 2 := by
   have := h.fderiv_descent_le x y hf
   rwa [fderiv_eq_deriv_mul, dist_comm, Real.dist_eq, sq_abs] at this
 
+theorem deriv_descent_ge (h : LipschitzSmoothWith K f) (x y : ℝ) (hf : DifferentiableAt ℝ f x) :
+    f x + deriv f x * (y - x) - ↑K / 2 * (y - x) ^ 2 ≤ f y := by
+  have := h.fderiv_descent_ge x y hf
+  rwa [fderiv_eq_deriv_mul, dist_comm, Real.dist_eq, sq_abs] at this
+
 theorem deriv_sub_mul_le (h : LipschitzSmoothWith K f) (x y : ℝ)
     (hfx : DifferentiableAt ℝ f x) (hfy : DifferentiableAt ℝ f y) :
     (deriv f y - deriv f x) * (y - x) ≤ ↑K * (y - x) ^ 2 := by

Mathlib/Analysis/Calculus/LipschitzSmooth/FDeriv.lean

@@ -13,7 +13,7 @@ public import Mathlib.Analysis.Calculus.LipschitzSmooth.Basic
 
 Fréchet-derivative restatements of the `LipschitzSmoothWith` predicate. For differentiable
 `f`, `lineDeriv ℝ f x v = fderiv ℝ f x v` pointwise, and the predicate is equivalent to
-the corresponding descent inequality stated in `fderiv` form.
+the two-sided Taylor bound stated in `fderiv` form.
 -/
 
 public section
@@ -22,24 +22,40 @@ variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
 variable {K : NNReal} {f : F → ℝ}
 
 theorem lipschitzSmoothWith_iff_fderiv (hf : Differentiable ℝ f) : LipschitzSmoothWith K f ↔
-    ∀ x y : F, f y ≤ f x + fderiv ℝ f x (y - x) + ↑K / 2 * (dist x y) ^ 2 := by
+    ∀ x y : F, |f y - f x - fderiv ℝ f x (y - x)| ≤ ↑K / 2 * (dist x y) ^ 2 := by
   rw [lipschitzSmoothWith_iff_lineDeriv]
   refine forall_congr' fun x => forall_congr' fun y => ?_
   rw [(hf x).lineDeriv_eq_fderiv]
 
 namespace LipschitzSmoothWith
 
+theorem fderiv_abs_le (h : LipschitzSmoothWith K f) (x y : F) (hf : DifferentiableAt ℝ f x) :
+    |f y - f x - fderiv ℝ f x (y - x)| ≤ ↑K / 2 * (dist x y) ^ 2 := by
+  rw [← hf.lineDeriv_eq_fderiv]
+  exact h.lineDeriv_abs_le x y
+
 theorem fderiv_descent_le (h : LipschitzSmoothWith K f) (x y : F) (hf : DifferentiableAt ℝ f x) :
     f y ≤ f x + fderiv ℝ f x (y - x) + ↑K / 2 * (dist x y) ^ 2 := by
   rw [← hf.lineDeriv_eq_fderiv]
   exact h.lineDeriv_descent_le x y
 
+theorem fderiv_descent_ge (h : LipschitzSmoothWith K f) (x y : F) (hf : DifferentiableAt ℝ f x) :
+    f x + fderiv ℝ f x (y - x) - ↑K / 2 * (dist x y) ^ 2 ≤ f y := by
+  rw [← hf.lineDeriv_eq_fderiv]
+  exact h.lineDeriv_descent_ge x y
+
 theorem fderiv_apply_sub_le (h : LipschitzSmoothWith K f) (x y : F)
     (hfx : DifferentiableAt ℝ f x) (hfy : DifferentiableAt ℝ f y) :
     fderiv ℝ f y (y - x) - fderiv ℝ f x (y - x) ≤ ↑K * (dist x y) ^ 2 := by
   rw [← hfy.lineDeriv_eq_fderiv, ← hfx.lineDeriv_eq_fderiv]
   exact h.lineDeriv_apply_sub_le x y
 
+theorem fderiv_apply_sub_abs_le (h : LipschitzSmoothWith K f) (x y : F)
+    (hfx : DifferentiableAt ℝ f x) (hfy : DifferentiableAt ℝ f y) :
+    |fderiv ℝ f y (y - x) - fderiv ℝ f x (y - x)| ≤ ↑K * (dist x y) ^ 2 := by
+  rw [← hfy.lineDeriv_eq_fderiv, ← hfx.lineDeriv_eq_fderiv]
+  exact h.lineDeriv_apply_sub_abs_le x y
+
 theorem fderiv_sub_apply_le (h : LipschitzSmoothWith K f) (x y : F)
     (hfx : DifferentiableAt ℝ f x) (hfy : DifferentiableAt ℝ f y) :
     (fderiv ℝ f y - fderiv ℝ f x) (y - x) ≤ ↑K * (dist x y) ^ 2 := by

Mathlib/Analysis/Calculus/LipschitzSmooth/Gradient.lean

@@ -13,8 +13,8 @@ public import Mathlib.Analysis.Calculus.LipschitzSmooth.FDeriv
 
 On a Hilbert space `F`, the `LipschitzSmoothWith` predicate admits a gradient-form
 characterisation. For differentiable `f`, `fderiv ℝ f x (y - x) = ⟪∇ f x, y - x⟫`
-via Riesz representation (`inner_gradient_left`), and the descent inequality becomes
-`f y ≤ f x + ⟪∇ f x, y - x⟫ + K/2 · ‖y - x‖²`.
+via Riesz representation (`inner_gradient_left`), and the two-sided Taylor bound becomes
+`|f y - f x - ⟪∇ f x, y - x⟫| ≤ K/2 · ‖y - x‖²`.
 
 This file also defines the **`CocoerciveWith K f`** predicate (the conclusion of the
 Baillon-Haddad theorem) and the elementary direction `K`-cocoercive ⟹ `K`-Lipschitz
@@ -29,19 +29,32 @@ variable {K : NNReal} {f : F → ℝ}
 open scoped Gradient RealInnerProductSpace
 
 theorem lipschitzSmoothWith_iff_inner_gradient (hf : Differentiable ℝ f) :
-    LipschitzSmoothWith K f ↔ ∀ x y : F, f y ≤ f x + ⟪∇ f x, y - x⟫ + ↑K / 2 * ‖y - x‖ ^ 2 := by
+    LipschitzSmoothWith K f ↔
+      ∀ x y : F, |f y - f x - ⟪∇ f x, y - x⟫| ≤ ↑K / 2 * ‖y - x‖ ^ 2 := by
   rw [lipschitzSmoothWith_iff_fderiv hf]
   refine forall_congr' fun x => forall_congr' fun y => ?_
   rw [inner_gradient_left, dist_eq_norm']
 
 namespace LipschitzSmoothWith
 
+theorem inner_gradient_abs_le (h : LipschitzSmoothWith K f) (x y : F)
+    (hf : DifferentiableAt ℝ f x) :
+    |f y - f x - ⟪∇ f x, y - x⟫| ≤ ↑K / 2 * ‖y - x‖ ^ 2 := by
+  rw [inner_gradient_left, ← dist_eq_norm']
+  exact h.fderiv_abs_le x y hf
+
 theorem inner_gradient_descent_le (h : LipschitzSmoothWith K f) (x y : F)
     (hf : DifferentiableAt ℝ f x) :
     f y ≤ f x + ⟪∇ f x, y - x⟫ + ↑K / 2 * ‖y - x‖ ^ 2 := by
   rw [inner_gradient_left, ← dist_eq_norm']
   exact h.fderiv_descent_le x y hf
 
+theorem inner_gradient_descent_ge (h : LipschitzSmoothWith K f) (x y : F)
+    (hf : DifferentiableAt ℝ f x) :
+    f x + ⟪∇ f x, y - x⟫ - ↑K / 2 * ‖y - x‖ ^ 2 ≤ f y := by
+  rw [inner_gradient_left, ← dist_eq_norm']
+  exact h.fderiv_descent_ge x y hf
+
 theorem inner_gradient_sub_le (h : LipschitzSmoothWith K f) (x y : F)
     (hfx : DifferentiableAt ℝ f x) (hfy : DifferentiableAt ℝ f y) :
     ⟪∇ f y - ∇ f x, y - x⟫ ≤ ↑K * ‖y - x‖ ^ 2 := by