refactor(LipschitzSmooth): derive const from affine + add ContinuousAffineMap companion

- `lipschitzSmoothWith_const` now derived as a one-liner from
  `lipschitzSmoothWith_affine` with `ℓ = 0` (was duplicated proof).
- Add `lipschitzSmoothWith_continuousAffineMap` in `Algebra.lean` as the
  bundled `ContinuousAffineMap` companion to the linear+const form in
  `Basic.lean`. Mathematically cleanest statement, but stays in
  `Algebra.lean` since it pulls in `ContinuousAffineMap`.

Author: FordUniver

Mathlib/Analysis/Calculus/LipschitzSmooth/Algebra.lean

@@ -27,6 +27,13 @@ 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 (differentiable) is `(K₁ + K₂)`-smooth. -/

Mathlib/Analysis/Calculus/LipschitzSmooth/Basic.lean

@@ -124,13 +124,6 @@ end LipschitzSmoothWith
 
 /-! ### Algebraic preservation -/
 
-/-- A constant function is `0`-smooth. -/
-theorem lipschitzSmoothWith_const (c : ℝ) : LipschitzSmoothWith (0 : NNReal) (fun _ : F => c) :=
-  lipschitzSmoothWith_iff_lineDeriv.mpr fun x y => by
-    have h : HasFDerivAt (fun _ : F => c) (0 : F →L[ℝ] ℝ) x := hasFDerivAt_const c x
-    rw [(h.hasLineDerivAt (y - x)).lineDeriv]
-    simp
-
 /-- An affine function `y ↦ ℓ y + c` is `0`-smooth. -/
 theorem lipschitzSmoothWith_affine (ℓ : F →L[ℝ] ℝ) (c : ℝ) :
     LipschitzSmoothWith (0 : NNReal) (fun y => ℓ y + c) :=
@@ -140,3 +133,7 @@ theorem lipschitzSmoothWith_affine (ℓ : F →L[ℝ] ℝ) (c : ℝ) :
     push_cast
     linarith
 
+/-- 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
+