feat(LipschitzSmooth/Continuity): finite-dim continuity via K-semiconcavity

Mathlib/Analysis/Calculus/LipschitzSmooth/Continuity.lean

@@ -0,0 +1,146 @@
+/-
+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.ContDiff.RCLike
+public import Mathlib.Analysis.Calculus.LipschitzSmooth.FDeriv
+public import Mathlib.Analysis.Convex.Continuous
+public import Mathlib.Analysis.InnerProductSpace.Basic
+public import Mathlib.Analysis.InnerProductSpace.Calculus
+
+/-!
+# Continuity of Lipschitz-smooth functions on a finite-dim Hilbert space
+
+In a finite-dimensional real inner-product space, a `K`-smooth function is locally
+Lipschitz, hence continuous — without any convexity hypothesis on `f` and without
+presupposing differentiability.
+
+The proof routes through the **K-semiconcavity decomposition**: the upper-bound side
+of the two-sided abs predicate implies that `g(x) := f x - K/2 ‖x‖²` is concave on the
+whole space (Cannarsa-Sinestrari, *Semiconcave Functions, Hamilton-Jacobi Equations,
+and Optimal Control* (2004), Proposition 1.1.3(a)⇔(c) p.2). Mathlib's
+`ConcaveOn.locallyLipschitz` (which requires `[FiniteDimensional ℝ F]`) then gives
+local Lipschitz of `g`, and adding back the locally Lipschitz `K/2 ‖x‖²` recovers `f`.
+
+The `[FiniteDimensional]` hypothesis is necessary: in infinite-dim, a discontinuous
+linear functional `ℓ : F → ℝ` satisfies `LipschitzSmoothWith 0 ℓ` but fails continuity
+(Bauschke-Combettes, *Convex Analysis and Monotone Operator Theory in Hilbert Spaces*
+(2017), Example 8.42 p.151). The `[InnerProductSpace]` restriction is for the
+parallelogram identity used in the K-semiconcavity decomposition; the result extends
+to general finite-dim real normed spaces via norm-equivalence transfer (deferred).
+
+## Main results
+
+- `LipschitzSmoothWith.concaveOn_sub_half_sq_norm`: the semiconcavity decomposition
+  (any dim, Hilbert).
+- `LipschitzSmoothWith.locallyLipschitz`: corollary (finite-dim Hilbert).
+- `LipschitzSmoothWith.continuous`: corollary (finite-dim Hilbert).
+-/
+
+public section
+
+variable {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℝ F]
+variable {K : NNReal} {f : F → ℝ}
+
+namespace LipschitzSmoothWith
+
+open scoped InnerProductSpace RealInnerProductSpace
+
+/-- **K-semiconcavity decomposition.** A `K`-smooth function `f` on a real
+inner-product space makes `f - K/2 ‖·‖²` concave on the whole space.
+
+The proof is the standard averaging argument: applying the predicate's upper-bound
+direction at `(z, x)` and `(z, y)` with `z = a • x + b • y` (and `a + b = 1`), the
+line-derivative terms cancel by positive homogeneity (since `x - z` and `y - z` are
+anti-parallel scalar multiples of `x - y`), leaving the semiconcavity inequality
+`a • f x + b • f y ≤ f z + K/2 · a b ‖x - y‖²`. The parallelogram identity
+`a‖x‖² + b‖y‖² - ‖a•x + b•y‖² = a b ‖x - y‖²` (specific to inner-product spaces)
+then converts this to `ConcaveOn` form.
+
+See Cannarsa-Sinestrari (2004) Proposition 1.1.3 (p.2) for the equivalence between
+"K-semiconcave with linear modulus" and "`f - K/2 ‖·‖²` concave". -/
+theorem concaveOn_sub_half_sq_norm (h : LipschitzSmoothWith K f) :
+    ConcaveOn ℝ Set.univ (fun x : F => f x - ↑K / 2 * ‖x‖^2) := by
+  refine ⟨convex_univ, fun x _ y _ a b ha hb hab => ?_⟩
+  set z : F := a • x + b • y with hz_def
+  have hxz : x - z = b • (x - y) := by
+    rw [hz_def]; match_scalars <;> linarith
+  have hyz : y - z = (-a) • (x - y) := by
+    rw [hz_def]; match_scalars <;> linarith
+  have hux := h.lineDeriv_descent_le z x
+  have huy := h.lineDeriv_descent_le z y
+  rw [hxz, lineDeriv_smul, smul_eq_mul,
+      show dist z x = b * ‖x - y‖ by
+        rw [dist_eq_norm', hxz, norm_smul, Real.norm_eq_abs, abs_of_nonneg hb],
+      mul_pow] at hux
+  rw [hyz, lineDeriv_smul, smul_eq_mul,
+      show dist z y = a * ‖x - y‖ by
+        rw [dist_eq_norm', hyz, norm_smul, Real.norm_eq_abs, abs_neg, abs_of_nonneg ha],
+      mul_pow] at huy
+  -- Inner-product identity: a‖x‖² + b‖y‖² - ‖z‖² = a*b*‖x-y‖²
+  have inner_id : a * ‖x‖^2 + b * ‖y‖^2 - ‖z‖^2 = a * b * ‖x - y‖^2 := by
+    have e₁ : ‖z‖^2 = a^2 * ‖x‖^2 + 2 * (a * b) * ⟪x, y⟫_ℝ + b^2 * ‖y‖^2 := by
+      rw [hz_def, @norm_add_sq_real F, norm_smul, norm_smul, Real.norm_eq_abs,
+        Real.norm_eq_abs, abs_of_nonneg ha, abs_of_nonneg hb, real_inner_smul_left,
+        real_inner_smul_right]; ring
+    have e₂ : ‖x - y‖^2 = ‖x‖^2 - 2 * ⟪x, y⟫_ℝ + ‖y‖^2 := @norm_sub_sq_real F _ _ _ _
+    linear_combination -e₁ - a*b * e₂ - (a * ‖x‖^2 + b * ‖y‖^2) * hab
+  -- Combine the two upper bounds via polynomial identities under hab
+  set L := lineDeriv ℝ f z (x - y) with hL_def
+  set s := ‖x - y‖^2 with hs_def
+  have hux' : a * f x ≤ a * f z + a * b * L + ↑K / 2 * (a * b^2 * s) := by
+    have h1 := mul_le_mul_of_nonneg_left hux ha
+    nlinarith [h1]
+  have huy' : b * f y ≤ b * f z - a * b * L + ↑K / 2 * (b * a^2 * s) := by
+    have h1 := mul_le_mul_of_nonneg_left huy hb
+    nlinarith [h1]
+  have coef_eq : a * b^2 + b * a^2 = a * b := by linear_combination a * b * hab
+  have fz_eq : a * f z + b * f z = f z := by linear_combination f z * hab
+  have rhs_eq :
+      (a * f z + a * b * L + ↑K / 2 * (a * b^2 * s))
+        + (b * f z - a * b * L + ↑K / 2 * (b * a^2 * s)) = f z + ↑K / 2 * (a * b * s) := by
+    linear_combination fz_eq + (↑K / 2 * s) * coef_eq
+  have sum_ineq : a * f x + b * f y ≤ f z + ↑K / 2 * (a * b * s) := by
+    linarith [hux', huy', rhs_eq]
+  have inner_id_K : ↑K / 2 * (a * ‖x‖^2 + b * ‖y‖^2 - ‖z‖^2) = ↑K / 2 * (a * b * s) := by
+    linear_combination (↑K / 2) * inner_id
+  have goal : a * (f x - ↑K / 2 * ‖x‖^2) + b * (f y - ↑K / 2 * ‖y‖^2) ≤
+      f z - ↑K / 2 * ‖z‖^2 := by
+    linarith [sum_ineq, inner_id_K]
+  simpa using goal
+
+end LipschitzSmoothWith
+
+section FiniteDim
+
+variable [FiniteDimensional ℝ F]
+
+namespace LipschitzSmoothWith
+
+/-- A `K`-smooth function on a finite-dim real inner-product space is locally Lipschitz.
+
+Proof: the K-semiconcavity decomposition `f - K/2 ‖·‖²` concave (from
+`concaveOn_sub_half_sq_norm`), combined with mathlib's `ConcaveOn.locallyLipschitz`
+(which requires `[FiniteDimensional ℝ F]`), gives local Lipschitz of the concave
+part. Adding back the locally Lipschitz `K/2 ‖·‖²` (via `ContDiff.locallyLipschitz`
+applied to `contDiff_norm_sq`) recovers `f`. -/
+theorem locallyLipschitz (h : LipschitzSmoothWith K f) : LocallyLipschitz f := by
+  have hcon : LocallyLipschitz (fun x : F => f x - ↑K / 2 * ‖x‖^2) :=
+    h.concaveOn_sub_half_sq_norm.locallyLipschitz
+  have hquad : LocallyLipschitz (fun x : F => ↑K / 2 * ‖x‖^2) :=
+    (contDiff_const.mul (contDiff_norm_sq (𝕜 := ℝ))).locallyLipschitz
+  have heq : f = (fun x : F => f x - ↑K / 2 * ‖x‖^2) + fun x => ↑K / 2 * ‖x‖^2 := by
+    funext x; simp only [Pi.add_apply]; ring
+  rw [heq]
+  exact hcon.add hquad
+
+/-- A `K`-smooth function on a finite-dim real inner-product space is continuous. -/
+theorem continuous (h : LipschitzSmoothWith K f) : Continuous f :=
+  h.locallyLipschitz.continuous
+
+end LipschitzSmoothWith
+
+end FiniteDim