refactor(LipschitzSmooth/Algebra): rewrite hypothesis-free under abs predicate

The two-sided abs form of `LipschitzSmoothWith` (predicated on the
weakest form `lineDeriv`) implies line-differentiability everywhere via
`LipschitzSmoothWith.hasLineDerivAt`, so the algebraic preservation
lemmas no longer require any `Differentiable ℝ f` hypothesis:

- `add` works in pure `lineDeriv` form by computing
  `HasLineDerivAt (f₁ + f₂)` from the two pointwise `hasLineDerivAt`
  witnesses (via `HasDerivAt.add`), then chaining the triangle
  inequality with the two abs bounds.
- `const_smul` analogously via `HasDerivAt.const_smul` and `abs_mul`
  plus `abs_of_nonneg` (since `c : NNReal ≥ 0`).
- `neg` becomes trivial under the abs predicate (it was not provable
  under the old one-sided descent form), with the *same* constant `K`.

Also fix the `lipschitzSmoothWith_affine` proof in `Basic.lean` (the
post-`map_sub` goal is now `|0| ≤ 0` rather than the old descent
`linarith`-trivial goal, so the closing tactic switches to `simp`).

The module docstring is updated to drop the (now-false) "not closed
under negation" caveat — that was a consequence of the one-sided form
and disappears in the two-sided form. The deferred-follow-up sorry on
`comp_continuousAffineMap` is unchanged.

Author: FordUniver

Mathlib/Analysis/Calculus/LipschitzSmooth/Algebra.lean

@@ -13,12 +13,14 @@ public import Mathlib.Analysis.Normed.Affine.ContinuousAffineMap
 
 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`).
+`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`. Note that `LipschitzSmoothWith` is *not*
-closed under negation or negative scaling — the descent inequality is one-sided, mirroring
-the asymmetry of concavity.
+`Mathlib.Analysis.Calculus.LipschitzSmooth.Basic`. None of the lemmas here require any
+differentiability hypothesis — `LipschitzSmoothWith` implies line-differentiability
+everywhere via `LipschitzSmoothWith.hasLineDerivAt`.
 -/
 
 public section
@@ -36,30 +38,55 @@ theorem lipschitzSmoothWith_continuousAffineMap (A : F →ᴬ[ℝ] ℝ) :
 
 namespace LipschitzSmoothWith
 
-/-- Sum of `K₁`-smooth and `K₂`-smooth (differentiable) is `(K₁ + K₂)`-smooth. -/
-theorem add (h₁ : LipschitzSmoothWith K₁ f₁) (h₂ : LipschitzSmoothWith K₂ f₂)
-    (hf₁ : Differentiable ℝ f₁) (hf₂ : Differentiable ℝ f₂) :
-    LipschitzSmoothWith (K₁ + K₂) (f₁ + f₂) := by
-  rw [lipschitzSmoothWith_iff_fderiv (hf₁.add hf₂)]
-  intro x y
-  rw [fderiv_add (hf₁ x) (hf₂ x), ContinuousLinearMap.add_apply]
-  have h1 := (lipschitzSmoothWith_iff_fderiv hf₁).mp h₁ x y
-  have h2 := (lipschitzSmoothWith_iff_fderiv hf₂).mp h₂ x y
-  push_cast
-  simp only [Pi.add_apply]
-  linarith
+/-- 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
 
-/-- Scaling a `K`-smooth (differentiable) function by `c : NNReal` gives `(c * K)`-smoothness. -/
-theorem const_smul (h : LipschitzSmoothWith K f) (hf : Differentiable ℝ f) (c : NNReal) :
-    LipschitzSmoothWith (c * K) ((c : ℝ) • f) := by
-  have hcf : Differentiable ℝ ((c : ℝ) • f) := hf.const_smul (c : ℝ)
-  rw [lipschitzSmoothWith_iff_fderiv hcf]
-  intro x y
-  rw [fderiv_const_smul (hf x) (c : ℝ), ContinuousLinearMap.smul_apply]
-  have hd := (lipschitzSmoothWith_iff_fderiv hf).mp h x y
-  push_cast
-  simp only [Pi.smul_apply, smul_eq_mul]
-  nlinarith [c.coe_nonneg, sq_nonneg (dist x y)]
+/-- 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'`. -/

Mathlib/Analysis/Calculus/LipschitzSmooth/Basic.lean

@@ -130,8 +130,7 @@ theorem lipschitzSmoothWith_affine (ℓ : F →L[ℝ] ℝ) (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]
-    push_cast
-    linarith
+    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