diff --git a/Mathlib.lean b/Mathlib.lean
index 25322c6b37cb10..fec96c4e71c0ff 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -1831,6 +1831,10 @@ public import Mathlib.Analysis.Calculus.LineDeriv.Basic
 public import Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts
 public import Mathlib.Analysis.Calculus.LineDeriv.Measurable
 public import Mathlib.Analysis.Calculus.LineDeriv.QuadraticMap
+public import Mathlib.Analysis.Calculus.LipschitzSmooth.Basic
+public import Mathlib.Analysis.Calculus.LipschitzSmooth.Deriv
+public import Mathlib.Analysis.Calculus.LipschitzSmooth.FDeriv
+public import Mathlib.Analysis.Calculus.LipschitzSmooth.Gradient
 public import Mathlib.Analysis.Calculus.LocalExtr.Basic
 public import Mathlib.Analysis.Calculus.LocalExtr.LineDeriv
 public import Mathlib.Analysis.Calculus.LocalExtr.Polynomial
@@ -1951,10 +1955,12 @@ public import Mathlib.Analysis.Convex.EGauge
 public import Mathlib.Analysis.Convex.Exposed
 public import Mathlib.Analysis.Convex.Extrema
 public import Mathlib.Analysis.Convex.Extreme
+public import Mathlib.Analysis.Convex.FDeriv
 public import Mathlib.Analysis.Convex.Function
 public import Mathlib.Analysis.Convex.FunctionTopology
 public import Mathlib.Analysis.Convex.Gauge
 public import Mathlib.Analysis.Convex.GaugeRescale
+public import Mathlib.Analysis.Convex.Gradient
 public import Mathlib.Analysis.Convex.Hull
 public import Mathlib.Analysis.Convex.Independent
 public import Mathlib.Analysis.Convex.Integral
@@ -1962,6 +1968,7 @@ public import Mathlib.Analysis.Convex.Intrinsic
 public import Mathlib.Analysis.Convex.Jensen
 public import Mathlib.Analysis.Convex.Join
 public import Mathlib.Analysis.Convex.KreinMilman
+public import Mathlib.Analysis.Convex.LineDeriv
 public import Mathlib.Analysis.Convex.LinearIsometry
 public import Mathlib.Analysis.Convex.Measure
 public import Mathlib.Analysis.Convex.MetricSpace
diff --git a/Mathlib/Analysis/Calculus/LipschitzSmooth/Basic.lean b/Mathlib/Analysis/Calculus/LipschitzSmooth/Basic.lean
new file mode 100644
index 00000000000000..5bdcc496600923
--- /dev/null
+++ b/Mathlib/Analysis/Calculus/LipschitzSmooth/Basic.lean
@@ -0,0 +1,134 @@
+/-
+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.LineDeriv.Basic
+
+/-!
+# Lipschitz smoothness
+
+A function `f : E → F` between real normed vector spaces 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) ^ 2`
+
+for all `x, y`. The predicate uses `lineDeriv` so as not to presuppose Fréchet
+differentiability; equivalent characterisations in `fderiv`, 1D `deriv`, and
+Hilbert-space gradient form live in the sibling files in this directory.
+
+This two-sided (norm) form is orientation-agnostic (closed under `f ↦ -f`) —
+matching, for real-valued `f`, the textbook notion of L-smoothness (Lipschitz
+gradient, the class `C^{1,1}`). The one-sided descent bounds require an order
+on the codomain and are stated for real-valued `f` in a dedicated section.
+-/
+
+public section
+
+variable {E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
+  [NormedAddCommGroup F] [NormedSpace ℝ F]
+
+/-- A function `f : E → F` between real normed vector spaces 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) ^ 2` for all `x, y`.
+
+The predicate is two-sided (norm), so closed under `f ↦ -f` and matching, for
+real-valued `f`, 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.
+
+Equivalent characterisations in `fderiv`, `gradient`, and `deriv` form are
+provided in the sibling files, predicated on `Differentiable` where useful.
+The one-sided descent bounds, which require an order on the codomain, are
+stated for real-valued `f`. -/
+def LipschitzSmoothWith (K : NNReal) (f : E → F) :=
+  ∀ (x y : E), ‖f y - f x - lineDeriv ℝ f x (y - x)‖ ≤ K / 2 * (dist x y) ^ 2
+
+theorem lipschitzSmoothWith_iff_lineDeriv {K : NNReal} {f : E → F} : LipschitzSmoothWith K f ↔
+    ∀ x y : E, ‖f y - f x - lineDeriv ℝ f x (y - x)‖ ≤ K / 2 * (dist x y) ^ 2 := Iff.rfl
+
+namespace LipschitzSmoothWith
+
+variable {K : NNReal} {f : E → F}
+
+/-- The two-sided quadratic bound on the first-order Taylor remainder, restated
+from the definition for dot notation. -/
+theorem lineDeriv_norm_le (h : LipschitzSmoothWith K f) (x y : E) :
+    ‖f y - f x - lineDeriv ℝ f x (y - x)‖ ≤ K / 2 * (dist x y) ^ 2 := h x y
+
+/-- Two-sided bound on the variation of the line derivative along `y - x`. -/
+theorem lineDeriv_apply_sub_norm_le (h : LipschitzSmoothWith K f) (x y : E) :
+    ‖lineDeriv ℝ f y (y - x) - lineDeriv ℝ f x (y - x)‖ ≤ K * (dist x y) ^ 2 := by
+  have hyx := h.lineDeriv_norm_le y x
+  rw [← neg_sub y x, lineDeriv_neg, sub_neg_eq_add, dist_comm] at hyx
+  have key := (norm_add_le _ _).trans (add_le_add hyx (h.lineDeriv_norm_le x y))
+  rw [show f x - f y + lineDeriv ℝ f y (y - x) + (f y - f x - lineDeriv ℝ f x (y - x))
+      = lineDeriv ℝ f y (y - x) - lineDeriv ℝ f x (y - x) from by abel] at key
+  linarith
+
+/-- `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 : E) :
+    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, Real.norm_eq_abs]
+  have hpred := h x (x + t • v)
+  rw [show (x + t • v) - x = t • v from by abel, lineDeriv_smul,
+      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 : E) :
+    LineDifferentiableAt ℝ f x v :=
+  (h.hasLineDerivAt x v).lineDifferentiableAt
+
+/-! ### Real-valued functions
+
+The one-sided (order-based) bounds require an order on the codomain, so they are
+stated for real-valued `f`. The norm and the absolute value agree on `ℝ`
+(`Real.norm_eq_abs`), so the two-sided bounds above apply verbatim. -/
+
+section Real
+
+variable {f : E → ℝ}
+
+/-- The quadratic upper bound on `f y`, traditionally called the *descent lemma*. -/
+theorem lineDeriv_descent_le (h : LipschitzSmoothWith K f) (x y : E) :
+    f y ≤ f x + lineDeriv ℝ f x (y - x) + K / 2 * (dist x y) ^ 2 := by
+  linarith [(abs_le.mp (h.lineDeriv_norm_le x y)).2]
+
+/-- The quadratic lower bound on `f y`: the descent lemma applied to `-f`. -/
+theorem lineDeriv_descent_ge (h : LipschitzSmoothWith K f) (x y : E) :
+    f x + lineDeriv ℝ f x (y - x) - K / 2 * (dist x y) ^ 2 ≤ f y := by
+  linarith [(abs_le.mp (h.lineDeriv_norm_le x y)).1]
+
+/-- One-sided bound on the variation of the line derivative along `y - x`. -/
+theorem lineDeriv_apply_sub_le (h : LipschitzSmoothWith K f) (x y : E) :
+    lineDeriv ℝ f y (y - x) - lineDeriv ℝ f x (y - x) ≤ K * (dist x y) ^ 2 :=
+  le_of_abs_le (h.lineDeriv_apply_sub_norm_le x y)
+
+/-- The one-sided variation bound in functional form: the difference of
+line-derivative maps applied to `y - x`. -/
+theorem lineDeriv_sub_apply_le (h : LipschitzSmoothWith K f) (x y : E) :
+    (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
+
+end Real
+
+end LipschitzSmoothWith
diff --git a/Mathlib/Analysis/Calculus/LipschitzSmooth/Deriv.lean b/Mathlib/Analysis/Calculus/LipschitzSmooth/Deriv.lean
new file mode 100644
index 00000000000000..066fe7718597b8
--- /dev/null
+++ b/Mathlib/Analysis/Calculus/LipschitzSmooth/Deriv.lean
@@ -0,0 +1,93 @@
+/-
+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.Deriv.Basic
+public import Mathlib.Analysis.Calculus.LipschitzSmooth.FDeriv
+
+/-!
+# Lipschitz smoothness in 1D via the derivative
+
+For a `K`-smooth function `f : ℝ → F`, the Taylor bound takes its 1D form
+
+`‖f y - f x - (y - x) • deriv f x‖ ≤ K/2 · (y - x)²`,
+
+lifted from the Fréchet-derivative form in
+`Mathlib.Analysis.Calculus.LipschitzSmooth.FDeriv` via `fderiv_eq_smul_deriv`.
+For real-valued `f` the one-sided bounds take their classical 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)²`,
+
+with the scalar action spelled as multiplication (`smul_eq_mul` bridges the two).
+-/
+
+public section
+
+variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
+variable {K : NNReal} {f : ℝ → F}
+
+theorem lipschitzSmoothWith_iff_deriv (hf : Differentiable ℝ f) : LipschitzSmoothWith K f ↔
+    ∀ x y : ℝ, ‖f y - f x - (y - x) • deriv f x‖ ≤ K / 2 * (y - x) ^ 2 := by
+  rw [lipschitzSmoothWith_iff_fderiv hf]
+  refine forall_congr' fun x => forall_congr' fun y => ?_
+  rw [fderiv_eq_smul_deriv, dist_comm, Real.dist_eq, sq_abs]
+
+namespace LipschitzSmoothWith
+
+theorem deriv_norm_le (h : LipschitzSmoothWith K f) (x y : ℝ) (hf : DifferentiableAt ℝ f x) :
+    ‖f y - f x - (y - x) • deriv f x‖ ≤ K / 2 * (y - x) ^ 2 := by
+  simpa only [fderiv_eq_smul_deriv, dist_comm x y, Real.dist_eq, sq_abs]
+    using h.fderiv_norm_le x y hf
+
+/-! ### Real-valued functions -/
+
+section Real
+
+variable {f : ℝ → ℝ}
+
+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
+  simpa only [fderiv_eq_deriv_mul, dist_comm x y, Real.dist_eq, sq_abs]
+    using h.fderiv_descent_le x y hf
+
+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
+  simpa only [fderiv_eq_deriv_mul, dist_comm x y, Real.dist_eq, sq_abs]
+    using h.fderiv_descent_ge x y hf
+
+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
+  simpa only [sub_apply, fderiv_eq_deriv_mul, ← sub_mul, dist_comm x y, Real.dist_eq, sq_abs]
+    using h.fderiv_sub_apply_le x y hfx hfy
+
+end Real
+
+end LipschitzSmoothWith
+
+/-! ### Lipschitz constants of `fderiv` versus `deriv` -/
+
+section Real
+
+variable {f : ℝ → ℝ}
+
+/-- For `f : ℝ → ℝ`, the Lipschitz constants of `fderiv ℝ f` and `deriv f` coincide:
+`deriv f` is the composition of `fderiv ℝ f` with the isometry
+`(ContinuousLinearMap.toSpanSingletonLIE ℝ ℝ).symm` (evaluation at `1`). -/
+theorem lipschitzWith_fderiv_iff_lipschitzWith_deriv :
+    LipschitzWith K (fderiv ℝ f) ↔ LipschitzWith K (deriv f) :=
+  ((ContinuousLinearMap.toSpanSingletonLIE ℝ ℝ).symm.isometry.lipschitzWith_iff K).symm
+
+/-! ### Descent lemma (1D) -/
+
+/-- **Descent lemma (1D).** If `f : ℝ → ℝ` is differentiable and its derivative is
+`K`-Lipschitz, then `f` is `K`-smooth. -/
+theorem Differentiable.lipschitzSmoothWith_of_lipschitzWith_deriv
+    (hf : Differentiable ℝ f) (hL : LipschitzWith K (deriv f)) : LipschitzSmoothWith K f :=
+  hf.lipschitzSmoothWith_of_lipschitzWith (lipschitzWith_fderiv_iff_lipschitzWith_deriv.mpr hL)
+
+end Real
diff --git a/Mathlib/Analysis/Calculus/LipschitzSmooth/FDeriv.lean b/Mathlib/Analysis/Calculus/LipschitzSmooth/FDeriv.lean
new file mode 100644
index 00000000000000..a00bd0fa63fea1
--- /dev/null
+++ b/Mathlib/Analysis/Calculus/LipschitzSmooth/FDeriv.lean
@@ -0,0 +1,154 @@
+/-
+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.FDeriv.Basic
+public import Mathlib.Analysis.Calculus.LipschitzSmooth.Basic
+public import Mathlib.Analysis.Normed.Affine.AddTorsor
+public import Mathlib.Analysis.SpecialFunctions.Integrals.Basic
+public import Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
+
+/-!
+# Lipschitz smoothness via the Fréchet derivative
+
+Fréchet-derivative restatements of the `LipschitzSmoothWith` predicate for
+`f : E → F`. For differentiable `f`, `lineDeriv ℝ f x v = fderiv ℝ f x v`
+pointwise, and the predicate is equivalent to the two-sided Taylor bound stated
+in `fderiv` form. The one-sided descent bounds require an order on the codomain
+and are stated for real-valued `f` in a dedicated section.
+
+This file also defines the segment-pointwise predicate `LipschitzSmoothOnSegmentWith` and
+proves the **descent lemma**: a differentiable function with `K`-Lipschitz Fréchet derivative
+is `K`-smooth. The proof integrates the segment-pointwise norm-bound along the segment from
+`x` to `y` using the fundamental theorem of calculus.
+-/
+
+public section
+
+variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
+variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
+variable {K : NNReal} {f : E → F}
+
+theorem lipschitzSmoothWith_iff_fderiv (hf : Differentiable ℝ f) : LipschitzSmoothWith K f ↔
+    ∀ x y : E, ‖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_norm_le (h : LipschitzSmoothWith K f) (x y : E) (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_norm_le x y
+
+theorem fderiv_apply_sub_norm_le (h : LipschitzSmoothWith K f) (x y : E)
+    (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_norm_le x y
+
+/-! ### Real-valued functions -/
+
+section Real
+
+variable {f : E → ℝ}
+
+theorem fderiv_descent_le (h : LipschitzSmoothWith K f) (x y : E) (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 : E) (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 : E)
+    (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_sub_apply_le (h : LipschitzSmoothWith K f) (x y : E)
+    (hfx : DifferentiableAt ℝ f x) (hfy : DifferentiableAt ℝ f y) :
+    (fderiv ℝ f y - fderiv ℝ f x) (y - x) ≤ K * (dist x y) ^ 2 := by
+  rw [sub_apply]
+  exact h.fderiv_apply_sub_le x y hfx hfy
+
+end Real
+
+end LipschitzSmoothWith
+
+/-! ### Descent lemma -/
+
+open AffineMap MeasureTheory
+
+/-- The pointwise two-sided Lipschitz-smoothness bound on the Fréchet derivative along the
+segment from `x` to `y`: `‖(fderiv ℝ f z - fderiv ℝ f x) (y - x)‖ ≤ K · dist x z · dist x y`
+for all `z ∈ [x -[ℝ] y]`. This is the segment-pointwise form that integrates to the descent
+inequality. -/
+abbrev LipschitzSmoothOnSegmentWith (K : NNReal) (f : E → F) : Prop :=
+  ∀ x y : E, ∀ z ∈ segment ℝ x y,
+    ‖(fderiv ℝ f z - fderiv ℝ f x) (y - x)‖ ≤ K * dist x z * dist x y
+
+/-- A `K`-Lipschitz Fréchet derivative implies the segment-pointwise smoothness bound.
+Direct from the operator-norm bound (`ContinuousLinearMap.le_opNorm`) plus the Lipschitz bound
+at the pair `(z, x)`. -/
+theorem LipschitzSmoothOnSegmentWith.of_lipschitzWith_fderiv
+    (hL : LipschitzWith K (fderiv ℝ f)) : LipschitzSmoothOnSegmentWith K f := fun x y z _ =>
+  calc ‖(fderiv ℝ f z - fderiv ℝ f x) (y - x)‖
+      ≤ ‖fderiv ℝ f z - fderiv ℝ f x‖ * ‖y - x‖ := ContinuousLinearMap.le_opNorm _ _
+    _ = dist (fderiv ℝ f x) (fderiv ℝ f z) * dist x y := by simp only [← dist_eq_norm']
+    _ ≤ K * dist x z * dist x y := mul_le_mul_of_nonneg_right (hL.dist_le_mul _ _) dist_nonneg
+
+/-- For a segment-pointwise Lipschitz-smooth function with continuous Fréchet derivative, the
+norm of the curve integral of `fderiv ℝ f z - fderiv ℝ f x` along the segment is
+bounded by `K/2 · (dist x y)²`. The quantitative FTC step of the descent lemma. -/
+theorem LipschitzSmoothOnSegmentWith.curveIntegral_norm_le
+      (h : LipschitzSmoothOnSegmentWith K f) (hcont : Continuous (fderiv ℝ f)) (x y : E) :
+      ‖∫ᶜ z in .segment x y, (fderiv ℝ f z - fderiv ℝ f x)‖ ≤ K / 2 * (dist x y) ^ 2 := by
+  have h_integrable : IntervalIntegrable
+      (fun t => (fderiv ℝ f (lineMap x y t) - fderiv ℝ f x) (y - x)) volume 0 1 :=
+    curveIntegrable_segment.mp <|
+      (hcont.curveIntegrable_segment).sub (curveIntegrable_segment_const _ x y)
+  calc ‖∫ᶜ z in .segment x y, (fderiv ℝ f z - fderiv ℝ f x)‖
+    _ = ‖∫ t in (0:ℝ)..1, (fderiv ℝ f (lineMap x y t) - fderiv ℝ f x) (y - x)‖ := by
+        rw [curveIntegral_segment]
+    _ ≤ ∫ t in (0:ℝ)..1, ‖(fderiv ℝ f (lineMap x y t) - fderiv ℝ f x) (y - x)‖ :=
+        intervalIntegral.norm_integral_le_integral_norm zero_le_one
+    _ ≤ ∫ t in (0:ℝ)..1, K * (dist x y) ^ 2 * t :=
+        intervalIntegral.integral_mono_on zero_le_one h_integrable.norm
+          (Continuous.intervalIntegrable (by fun_prop) _ _) (fun t ht =>
+            (h _ _ _ (segment_eq_image_lineMap ℝ x y ▸ Set.mem_image_of_mem _ ht)).trans_eq <| by
+              rw [dist_left_lineMap, Real.norm_of_nonneg ht.1]; ring)
+    _ = K * (dist x y) ^ 2 * ∫ t in (0:ℝ)..1, t := intervalIntegral.integral_const_mul _ _
+    _ = K / 2 * (dist x y) ^ 2 := by rw [integral_id]; ring
+
+/-- The segment-pointwise smoothness bound, together with differentiability and continuity of
+the Fréchet derivative, implies `K`-smoothness. The proof integrates the pointwise norm bound
+along the segment from `x` to `y` using FTC. -/
+theorem LipschitzSmoothOnSegmentWith.lipschitzSmoothWith [CompleteSpace F]
+    (hptwise : LipschitzSmoothOnSegmentWith K f) (hf : Differentiable ℝ f)
+    (hcont : Continuous (fderiv ℝ f)) : LipschitzSmoothWith K f := by
+  refine lipschitzSmoothWith_iff_lineDeriv.mpr fun x y => ?_
+  have heq : f y - f x - lineDeriv ℝ f x (y - x) =
+      ∫ᶜ z in .segment x y, (fderiv ℝ f z - fderiv ℝ f x) := calc
+    _ = f y - f x - (fderiv ℝ f x) (y - x) := by rw [(hf x).lineDeriv_eq_fderiv]
+    _ = (∫ᶜ z in .segment x y, fderiv ℝ f z) - ∫ᶜ _ in .segment x y, fderiv ℝ f x := by
+        rw [← curveIntegral_fderiv_segment (fun z _ => hf z) hcont.continuousOn,
+          ← curveIntegral_segment_const]
+    _ = ∫ᶜ z in .segment x y, (fderiv ℝ f z - fderiv ℝ f x) :=
+        (curveIntegral_fun_sub (hcont.curveIntegrable_segment)
+          (curveIntegrable_segment_const _ x y)).symm
+  rw [heq]
+  exact hptwise.curveIntegral_norm_le hcont x y
+
+/-- **Descent lemma.** If `f` is differentiable and its Fréchet derivative is
+`K`-Lipschitz, then `f` is `K`-smooth (without convexity assumption). -/
+theorem Differentiable.lipschitzSmoothWith_of_lipschitzWith [CompleteSpace F]
+    (hf : Differentiable ℝ f) (hL : LipschitzWith K (fderiv ℝ f)) : LipschitzSmoothWith K f :=
+  (LipschitzSmoothOnSegmentWith.of_lipschitzWith_fderiv hL).lipschitzSmoothWith hf hL.continuous
diff --git a/Mathlib/Analysis/Calculus/LipschitzSmooth/Gradient.lean b/Mathlib/Analysis/Calculus/LipschitzSmooth/Gradient.lean
new file mode 100644
index 00000000000000..0227a5b5de611e
--- /dev/null
+++ b/Mathlib/Analysis/Calculus/LipschitzSmooth/Gradient.lean
@@ -0,0 +1,98 @@
+/-
+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.Gradient.Basic
+public import Mathlib.Analysis.Calculus.LipschitzSmooth.FDeriv
+
+/-!
+# Lipschitz smoothness on a Hilbert space via the gradient
+
+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 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
+gradient.
+-/
+
+public section
+
+variable {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F]
+variable {K : NNReal} {f : F → ℝ}
+
+open InnerProductSpace
+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
+  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_norm_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
+  simpa only [inner_gradient_left, dist_eq_norm'] using h.fderiv_norm_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
+  simp only [← dist_eq_norm', inner_sub_left, inner_gradient_left, ← sub_apply]
+  exact h.fderiv_sub_apply_le x y hfx hfy
+
+end LipschitzSmoothWith
+
+/-! ### Cocoercivity -/
+
+/-- A function `f : F → ℝ` on a Hilbert space is **`K`-cocoercive** if its gradient satisfies
+`‖∇ f y - ∇ f x‖² ≤ K · ⟪∇ f y - ∇ f x, y - x⟫` for all `x, y`. Equivalent to the standard
+`(1/K)·‖·‖² ≤ ⟪·,·⟫` form when `0 < K`, but well-defined and meaningful even at `K = 0`
+(then forces `∇ f` constant). The conclusion of the Baillon-Haddad theorem. -/
+abbrev CocoerciveWith (K : NNReal) (f : F → ℝ) : Prop :=
+  ∀ x y : F, ‖∇ f y - ∇ f x‖ ^ 2 ≤ K * ⟪∇ f y - ∇ f x, y - x⟫
+
+/-- A `K`-cocoercive gradient is `K`-Lipschitz. (One direction of the Baillon-Haddad
+characterisation; the reverse requires convexity.) -/
+theorem CocoerciveWith.lipschitzWith_gradient (h : CocoerciveWith K f) : LipschitzWith K (∇ f) :=
+  lipschitzWith_iff_dist_le_mul.mpr fun x y => by
+    simp only [dist_eq_norm']
+    nlinarith [h x y, mul_nonneg K.coe_nonneg (norm_nonneg (y - x)),
+              mul_le_mul_of_nonneg_left (real_inner_le_norm (∇ f y - ∇ f x) (y - x)) K.coe_nonneg]
+
+/-! ### Riesz isomorphism for Lipschitz constants -/
+
+/-- The Riesz isomorphism identifies the Lipschitz constant of the Fréchet derivative with
+that of the gradient: `LipschitzWith K (fderiv ℝ f) ↔ LipschitzWith K (∇ f)`. Unconditional —
+the gradient is *defined* via Riesz from the fderiv, and Riesz is an isometry. -/
+theorem lipschitzWith_fderiv_iff_lipschitzWith_gradient :
+    LipschitzWith K (fderiv ℝ f) ↔ LipschitzWith K (∇ f) :=
+  toDual_comp_gradient (𝕜 := ℝ) (f := f) ▸ (toDual ℝ F).isometry.lipschitzWith_iff K
+
+/-! ### Descent lemma (Hilbert form) -/
+
+/-- **Descent lemma (Hilbert form).** If `f : F → ℝ` is differentiable on a Hilbert space
+and its gradient `∇ f` is `K`-Lipschitz, then `f` is `K`-smooth. -/
+theorem Differentiable.lipschitzSmoothWith_of_lipschitzWith_gradient
+    (hf : Differentiable ℝ f) (hL : LipschitzWith K (∇ f)) : LipschitzSmoothWith K f :=
+  hf.lipschitzSmoothWith_of_lipschitzWith (lipschitzWith_fderiv_iff_lipschitzWith_gradient.mpr hL)
diff --git a/Mathlib/Analysis/Convex/Deriv.lean b/Mathlib/Analysis/Convex/Deriv.lean
index 0e4fae608c2e01..f42a1ae91b387c 100644
--- a/Mathlib/Analysis/Convex/Deriv.lean
+++ b/Mathlib/Analysis/Convex/Deriv.lean
@@ -603,6 +603,22 @@ lemma deriv_le_slope (hfc : ConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy
     deriv f x ≤ slope f x y :=
   le_slope_of_hasDerivAt hfc hx hy hxy hfd.hasDerivAt
 
+/-- Additive form of the 1D first-order convexity inequality: for `f : ℝ → ℝ` convex on `S`,
+`x, y ∈ S` with `x < y`, and `f` differentiable at `x`, we have
+`f x + f' * (y - x) ≤ f y` where `f' = deriv f x`. -/
+lemma add_hasDerivAt_mul_le (hfc : ConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
+    (ha : HasDerivAt f f' x) :
+    f x + f' * (y - x) ≤ f y := by
+  have h := hfc.le_slope_of_hasDerivAt hx hy hxy ha
+  rw [slope_def_field, le_div_iff₀ (sub_pos.mpr hxy)] at h
+  linarith
+
+/-- Reformulation of `ConvexOn.add_hasDerivAt_mul_le` using `deriv`. -/
+lemma add_deriv_mul_le (hfc : ConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
+    (hfd : DifferentiableAt ℝ f x) :
+    f x + deriv f x * (y - x) ≤ f y :=
+  hfc.add_hasDerivAt_mul_le hx hy hxy hfd.hasDerivAt
+
 end left
 
 section right
@@ -774,6 +790,22 @@ lemma deriv_lt_slope (hfc : StrictConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S
     deriv f x < slope f x y :=
   hfc.lt_slope_of_hasDerivAt hx hy hxy hfd.hasDerivAt
 
+/-- Strict additive form of the 1D first-order convexity inequality: for `f : ℝ → ℝ` strictly
+convex on `S`, `x, y ∈ S` with `x < y`, and `f` differentiable at `x`, we have
+`f x + f' * (y - x) < f y` where `f' = deriv f x`. -/
+lemma add_hasDerivAt_mul_lt (hfc : StrictConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
+    (ha : HasDerivAt f f' x) :
+    f x + f' * (y - x) < f y := by
+  have h := hfc.lt_slope_of_hasDerivAt hx hy hxy ha
+  rw [slope_def_field, lt_div_iff₀ (sub_pos.mpr hxy)] at h
+  linarith
+
+/-- Reformulation of `StrictConvexOn.add_hasDerivAt_mul_lt` using `deriv`. -/
+lemma add_deriv_mul_lt (hfc : StrictConvexOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
+    (hfd : DifferentiableAt ℝ f x) :
+    f x + deriv f x * (y - x) < f y :=
+  hfc.add_hasDerivAt_mul_lt hx hy hxy hfd.hasDerivAt
+
 end left
 
 section right
@@ -892,6 +924,22 @@ lemma slope_le_deriv (hfc : ConcaveOn ℝ S f)
     slope f x y ≤ deriv f x :=
   hfc.slope_le_of_hasDerivAt hx hy hxy hfd.hasDerivAt
 
+/-- Additive form of the 1D first-order concavity inequality: for `f : ℝ → ℝ` concave on `S`,
+`x, y ∈ S` with `x < y`, and `f` differentiable at `x`, we have
+`f y ≤ f x + f' * (y - x)` where `f' = deriv f x`. -/
+lemma le_add_hasDerivAt_mul (hfc : ConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
+    (ha : HasDerivAt f f' x) :
+    f y ≤ f x + f' * (y - x) := by
+  have h := hfc.slope_le_of_hasDerivAt hx hy hxy ha
+  rw [slope_def_field, div_le_iff₀ (sub_pos.mpr hxy)] at h
+  linarith
+
+/-- Reformulation of `ConcaveOn.le_add_hasDerivAt_mul` using `deriv`. -/
+lemma le_add_deriv_mul (hfc : ConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
+    (hfd : DifferentiableAt ℝ f x) :
+    f y ≤ f x + deriv f x * (y - x) :=
+  hfc.le_add_hasDerivAt_mul hx hy hxy hfd.hasDerivAt
+
 end left
 
 section right
@@ -992,6 +1040,22 @@ lemma slope_lt_deriv (hfc : StrictConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈
     slope f x y < deriv f x :=
   hfc.slope_lt_of_hasDerivAt hx hy hxy hfd.hasDerivAt
 
+/-- Strict additive form of the 1D first-order concavity inequality: for `f : ℝ → ℝ` strictly
+concave on `S`, `x, y ∈ S` with `x < y`, and `f` differentiable at `x`, we have
+`f y < f x + f' * (y - x)` where `f' = deriv f x`. -/
+lemma lt_add_hasDerivAt_mul (hfc : StrictConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
+    (ha : HasDerivAt f f' x) :
+    f y < f x + f' * (y - x) := by
+  have h := hfc.slope_lt_of_hasDerivAt hx hy hxy ha
+  rw [slope_def_field, div_lt_iff₀ (sub_pos.mpr hxy)] at h
+  linarith
+
+/-- Reformulation of `StrictConcaveOn.lt_add_hasDerivAt_mul` using `deriv`. -/
+lemma lt_add_deriv_mul (hfc : StrictConcaveOn ℝ S f) (hx : x ∈ S) (hy : y ∈ S) (hxy : x < y)
+    (hfd : DifferentiableAt ℝ f x) :
+    f y < f x + deriv f x * (y - x) :=
+  hfc.lt_add_hasDerivAt_mul hx hy hxy hfd.hasDerivAt
+
 end left
 
 section right
diff --git a/Mathlib/Analysis/Convex/FDeriv.lean b/Mathlib/Analysis/Convex/FDeriv.lean
new file mode 100644
index 00000000000000..41b093638809c2
--- /dev/null
+++ b/Mathlib/Analysis/Convex/FDeriv.lean
@@ -0,0 +1,148 @@
+/-
+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.Convex.LineDeriv
+public import Mathlib.Analysis.Calculus.FDeriv.Basic
+
+/-!
+# First-order convexity inequality via the Fréchet derivative
+
+For `f : E → ℝ` convex on `s ⊆ E` and Fréchet-differentiable at `x ∈ s`, the first-order
+convexity inequality
+
+`f x + (fderiv ℝ f x) (y - x) ≤ f y`
+
+holds for `y ∈ s`. This is the Fréchet-derivative restatement of the line-derivative form
+in `Mathlib.Analysis.Convex.LineDeriv`, lifted via `HasFDerivAt.hasLineDerivAt`.
+
+The `HasFDerivAt`-flavoured statements are the primitives; the `fderiv`-flavoured ones are
+corollaries under `DifferentiableAt`.
+
+## Main results
+
+* `ConvexOn.add_fderiv_le` — the first-order convexity inequality (Fréchet form).
+* `ConvexOn.fderiv_sub_nonneg` — monotonicity along the chord.
+* `ConvexOn.isMinOn_of_fderiv_eq_zero` — the first-order optimality condition.
+* `convexOn_iff_add_fderiv_le` — iff converse: differentiability plus the first-order
+  inequality everywhere implies `ConvexOn`.
+
+Concave duals and strict variants are provided alongside.
+-/
+
+public section
+
+variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
+variable {f : E → ℝ} {s : Set E} {x y : E}
+
+namespace ConvexOn
+
+/-- For a convex function `f` with Fréchet derivative `f'` at `x`, the first-order inequality
+`f x + f' (y - x) ≤ f y` holds. -/
+theorem add_hasFDerivAt_le (hc : ConvexOn ℝ s f) (hx : x ∈ s) (hy : y ∈ s)
+    {f' : E →L[ℝ] ℝ} (hf : HasFDerivAt f f' x) :
+    f x + f' (y - x) ≤ f y :=
+  hc.add_hasLineDerivAt_le hx hy (hf.hasLineDerivAt _)
+
+/-- For a convex function `f` Fréchet-differentiable at `x`, the first-order inequality
+`f x + (fderiv ℝ f x) (y - x) ≤ f y` holds. -/
+theorem add_fderiv_le (hc : ConvexOn ℝ s f) (hx : x ∈ s) (hy : y ∈ s)
+    (hf : DifferentiableAt ℝ f x) :
+    f x + fderiv ℝ f x (y - x) ≤ f y :=
+  hc.add_hasFDerivAt_le hx hy hf.hasFDerivAt
+
+/-- Monotonicity of the Fréchet derivative along the chord: for convex `f` differentiable
+at `x` and `y`, `0 ≤ (fderiv ℝ f y - fderiv ℝ f x) (y - x)`. -/
+theorem fderiv_sub_nonneg (hc : ConvexOn ℝ s f) (hx : x ∈ s) (hy : y ∈ s)
+    (hfx : DifferentiableAt ℝ f x) (hfy : DifferentiableAt ℝ f y) :
+    0 ≤ (fderiv ℝ f y - fderiv ℝ f x) (y - x) := by
+  rw [sub_apply, ← hfx.lineDeriv_eq_fderiv, ← hfy.lineDeriv_eq_fderiv]
+  exact hc.lineDeriv_sub_nonneg hx hy hfx.lineDifferentiableAt hfy.lineDifferentiableAt
+
+/-- A convex function with a vanishing Fréchet derivative at an interior point of differentiability
+attains its minimum there. -/
+theorem isMinOn_of_fderiv_eq_zero (hc : ConvexOn ℝ s f) (hx : x ∈ s)
+    (hf : DifferentiableAt ℝ f x) (hgrad : fderiv ℝ f x = 0) :
+    IsMinOn f s x :=
+  fun y hy => by simpa [hgrad] using hc.add_fderiv_le hx hy hf
+
+end ConvexOn
+
+namespace ConcaveOn
+
+/-- For a concave function `f` with Fréchet derivative `f'` at `x`, the reverse first-order
+inequality `f y ≤ f x + f' (y - x)` holds. -/
+theorem le_add_hasFDerivAt (hc : ConcaveOn ℝ s f) (hx : x ∈ s) (hy : y ∈ s)
+    {f' : E →L[ℝ] ℝ} (hf : HasFDerivAt f f' x) :
+    f y ≤ f x + f' (y - x) :=
+  hc.le_add_hasLineDerivAt hx hy (hf.hasLineDerivAt _)
+
+/-- For a concave function `f` Fréchet-differentiable at `x`, the reverse first-order
+inequality `f y ≤ f x + (fderiv ℝ f x) (y - x)` holds. -/
+theorem le_add_fderiv (hc : ConcaveOn ℝ s f) (hx : x ∈ s) (hy : y ∈ s)
+    (hf : DifferentiableAt ℝ f x) :
+    f y ≤ f x + fderiv ℝ f x (y - x) :=
+  hc.le_add_hasFDerivAt hx hy hf.hasFDerivAt
+
+end ConcaveOn
+
+namespace StrictConvexOn
+
+/-- Strict variant of the first-order inequality for strictly convex `f` with Fréchet derivative
+`f'` at `x`, assuming `x ≠ y`: `f x + f' (y - x) < f y`. -/
+theorem add_hasFDerivAt_lt (hc : StrictConvexOn ℝ s f) (hx : x ∈ s) (hy : y ∈ s) (hxy : x ≠ y)
+    {f' : E →L[ℝ] ℝ} (hf : HasFDerivAt f f' x) :
+    f x + f' (y - x) < f y :=
+  hc.add_hasLineDerivAt_lt hx hy hxy (hf.hasLineDerivAt _)
+
+/-- Strict variant of the first-order inequality for strictly convex `f`:
+when `x ≠ y`, the inequality is strict. -/
+theorem add_fderiv_lt (hc : StrictConvexOn ℝ s f) (hx : x ∈ s) (hy : y ∈ s) (hxy : x ≠ y)
+    (hf : DifferentiableAt ℝ f x) :
+    f x + fderiv ℝ f x (y - x) < f y :=
+  hc.add_hasFDerivAt_lt hx hy hxy hf.hasFDerivAt
+
+end StrictConvexOn
+
+namespace StrictConcaveOn
+
+/-- Strict variant of the reverse first-order inequality for strictly concave `f` with Fréchet
+derivative `f'` at `x`, assuming `x ≠ y`: `f y < f x + f' (y - x)`. -/
+theorem lt_add_hasFDerivAt (hc : StrictConcaveOn ℝ s f) (hx : x ∈ s) (hy : y ∈ s) (hxy : x ≠ y)
+    {f' : E →L[ℝ] ℝ} (hf : HasFDerivAt f f' x) :
+    f y < f x + f' (y - x) :=
+  hc.lt_add_hasLineDerivAt hx hy hxy (hf.hasLineDerivAt _)
+
+/-- Strict variant of the reverse first-order inequality for strictly concave `f`: when `x ≠ y`,
+the inequality is strict. -/
+theorem lt_add_fderiv (hc : StrictConcaveOn ℝ s f) (hx : x ∈ s) (hy : y ∈ s) (hxy : x ≠ y)
+    (hf : DifferentiableAt ℝ f x) :
+    f y < f x + fderiv ℝ f x (y - x) :=
+  hc.lt_add_hasFDerivAt hx hy hxy hf.hasFDerivAt
+
+end StrictConcaveOn
+
+/-- A differentiable function is convex iff it satisfies the first-order inequality
+at every pair of points in `s`. -/
+theorem convexOn_iff_add_fderiv_le (hs : Convex ℝ s) (hf : ∀ x ∈ s, DifferentiableAt ℝ f x) :
+    ConvexOn ℝ s f ↔
+      ∀ x ∈ s, ∀ y ∈ s, f x + fderiv ℝ f x (y - x) ≤ f y := by
+  refine ⟨fun hc x hx y hy => hc.add_fderiv_le hx hy (hf x hx), fun H => ⟨hs, ?_⟩⟩
+  intro x hx y hy a b ha hb hab
+  set z := a • x + b • y with hz
+  set L := fderiv ℝ f z (x - y)
+  have hzs : z ∈ s := hs hx hy ha hb hab
+  have hb_eq : b = 1 - a := by linarith
+  have hzx : f z + b * L ≤ f x := by
+    simpa only [show x - z = b • (x - y) by rw [hz, hb_eq]; module, map_smul, smul_eq_mul]
+      using H z hzs x hx
+  have hzy : f z - a * L ≤ f y := by
+    simpa only [show y - z = -(a • (x - y)) by rw [hz, hb_eq]; module, map_neg, map_smul,
+      smul_eq_mul, ← sub_eq_add_neg] using H z hzs y hy
+  calc f z
+      = a * (f z + b * L) + b * (f z - a * L) := by linear_combination (f z) * hab.symm
+    _ ≤ a * f x + b * f y :=
+        add_le_add (mul_le_mul_of_nonneg_left hzx ha) (mul_le_mul_of_nonneg_left hzy hb)
diff --git a/Mathlib/Analysis/Convex/Gradient.lean b/Mathlib/Analysis/Convex/Gradient.lean
new file mode 100644
index 00000000000000..babbd33775e109
--- /dev/null
+++ b/Mathlib/Analysis/Convex/Gradient.lean
@@ -0,0 +1,110 @@
+/-
+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.Convex.FDeriv
+public import Mathlib.Analysis.Calculus.Gradient.Basic
+
+/-!
+# First-order convexity inequality via the gradient
+
+On a Hilbert space `F`, for `f : F → ℝ` convex on `s ⊆ F` and differentiable at `x ∈ s`,
+the first-order convexity inequality
+
+`f x + ⟪∇ f x, y - x⟫ ≤ f y`
+
+holds for `y ∈ s`. This is the gradient/inner-product restatement of the Fréchet form
+in `Mathlib.Analysis.Convex.FDeriv`, lifted via Riesz representation
+(`inner_gradient_left`).
+
+## Main results
+
+* `ConvexOn.add_inner_gradient_le` — the first-order convexity inequality (gradient form).
+* `ConvexOn.inner_gradient_sub_nonneg` — gradient monotonicity along the chord.
+* `ConvexOn.isMinOn_of_gradient_eq_zero` — the first-order optimality condition.
+* `convexOn_iff_add_inner_gradient_le` — iff converse.
+
+Concave duals and strict variants are provided alongside.
+-/
+
+public section
+
+variable {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F]
+variable {f : F → ℝ} {s : Set F} {x y : F}
+
+open InnerProductSpace
+open scoped Gradient RealInnerProductSpace
+
+namespace ConvexOn
+
+/-- For a convex function `f` differentiable at `x` on a Hilbert space, the first-order
+inequality `f x + ⟪∇ f x, y - x⟫ ≤ f y` holds. -/
+theorem add_inner_gradient_le (hc : ConvexOn ℝ s f) (hx : x ∈ s) (hy : y ∈ s)
+    (hf : DifferentiableAt ℝ f x) :
+    f x + ⟪∇ f x, y - x⟫ ≤ f y := by
+  rw [inner_gradient_left]
+  exact hc.add_fderiv_le hx hy hf
+
+/-- Monotonicity of the gradient along the chord: for convex `f` differentiable at `x`
+and `y`, `0 ≤ ⟪∇ f y - ∇ f x, y - x⟫`. -/
+theorem inner_gradient_sub_nonneg (hc : ConvexOn ℝ s f) (hx : x ∈ s) (hy : y ∈ s)
+    (hfx : DifferentiableAt ℝ f x) (hfy : DifferentiableAt ℝ f y) :
+    0 ≤ ⟪∇ f y - ∇ f x, y - x⟫ := by
+  rw [inner_sub_left, inner_gradient_left, inner_gradient_left,
+    ← sub_apply]
+  exact hc.fderiv_sub_nonneg hx hy hfx hfy
+
+/-- A convex function attains its minimum on `s` at any critical point: if `f` is convex on
+`s`, Fréchet-differentiable at `x ∈ s`, and `∇ f x = 0`, then `x` minimizes `f` on `s`.
+Multi-dimensional gradient analogue of `ConvexOn.isMinOn_of_rightDeriv_eq_zero`. -/
+theorem isMinOn_of_gradient_eq_zero (hc : ConvexOn ℝ s f) (hx : x ∈ s)
+    (hf : DifferentiableAt ℝ f x) (hg : ∇ f x = 0) :
+    IsMinOn f s x := fun _ hy => by
+  simpa [hg] using hc.add_inner_gradient_le hx hy hf
+
+end ConvexOn
+
+namespace ConcaveOn
+
+/-- For a concave function `f` differentiable at `x` on a Hilbert space, the reverse
+first-order inequality `f y ≤ f x + ⟪∇ f x, y - x⟫` holds. -/
+theorem le_add_inner_gradient (hc : ConcaveOn ℝ s f) (hx : x ∈ s) (hy : y ∈ s)
+    (hf : DifferentiableAt ℝ f x) :
+    f y ≤ f x + ⟪∇ f x, y - x⟫ := by
+  rw [inner_gradient_left]
+  exact hc.le_add_fderiv hx hy hf
+
+end ConcaveOn
+
+namespace StrictConvexOn
+
+/-- Strict variant of the first-order gradient inequality for strictly convex `f`. -/
+theorem add_inner_gradient_lt (hc : StrictConvexOn ℝ s f) (hx : x ∈ s) (hy : y ∈ s)
+    (hxy : x ≠ y) (hf : DifferentiableAt ℝ f x) :
+    f x + ⟪∇ f x, y - x⟫ < f y := by
+  rw [inner_gradient_left]
+  exact hc.add_fderiv_lt hx hy hxy hf
+
+end StrictConvexOn
+
+namespace StrictConcaveOn
+
+/-- Strict variant of the reverse first-order gradient inequality for strictly concave `f`. -/
+theorem lt_add_inner_gradient (hc : StrictConcaveOn ℝ s f) (hx : x ∈ s) (hy : y ∈ s)
+    (hxy : x ≠ y) (hf : DifferentiableAt ℝ f x) :
+    f y < f x + ⟪∇ f x, y - x⟫ := by
+  rw [inner_gradient_left]
+  exact hc.lt_add_fderiv hx hy hxy hf
+
+end StrictConcaveOn
+
+/-- A differentiable function on a Hilbert space is convex iff it satisfies the first-order
+gradient inequality at every pair of points in `s`. -/
+theorem convexOn_iff_add_inner_gradient_le (hs : Convex ℝ s)
+    (hf : ∀ x ∈ s, DifferentiableAt ℝ f x) :
+    ConvexOn ℝ s f ↔ ∀ x ∈ s, ∀ y ∈ s, f x + ⟪∇ f x, y - x⟫ ≤ f y := by
+  rw [convexOn_iff_add_fderiv_le hs hf]
+  simp_rw [inner_gradient_left]
diff --git a/Mathlib/Analysis/Convex/LineDeriv.lean b/Mathlib/Analysis/Convex/LineDeriv.lean
new file mode 100644
index 00000000000000..bf5b50cc44f9f3
--- /dev/null
+++ b/Mathlib/Analysis/Convex/LineDeriv.lean
@@ -0,0 +1,178 @@
+/-
+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.Convex.Deriv
+public import Mathlib.Analysis.Calculus.LineDeriv.Basic
+
+/-!
+# First-order convexity inequality via the directional derivative
+
+For `f : E → ℝ` convex on `s ⊆ E` and line-differentiable at `x ∈ s` in the direction
+`y - x`, the first-order convexity inequality
+
+`f x + lineDeriv ℝ f x (y - x) ≤ f y`
+
+holds for `y ∈ s`. This is the directional-derivative form of the convex subgradient
+inequality, lifted from the 1D case in `Mathlib.Analysis.Convex.Deriv` by restricting
+to the line segment between `x` and `y`.
+
+The `HasLineDerivAt`-flavoured statements are the primitives; the `lineDeriv`-flavoured
+ones are corollaries under `LineDifferentiableAt`.
+
+## Main results
+
+* `ConvexOn.add_lineDeriv_le` — the first-order convexity inequality
+  (line-derivative form).
+* `ConvexOn.lineDeriv_sub_nonneg` — monotonicity of the directional derivative along the
+  chord.
+
+Concave duals and strict variants are provided alongside.
+
+The iff converse to the first-order inequality lives at the Fréchet layer
+(`convexOn_iff_add_fderiv_le` in `Mathlib.Analysis.Convex.FDeriv`); the LineDeriv layer
+contains only forward implications.
+-/
+
+public section
+
+variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
+variable {f : E → ℝ} {s : Set E} {x y : E}
+
+private theorem lineMap_eq_add_smul_sub (x y : E) (t : ℝ) :
+    AffineMap.lineMap x y t = x + t • (y - x) := by
+  rw [AffineMap.lineMap_apply_module']; abel
+
+/-- The 1D restriction `t ↦ f (x + t • (y - x))` of a function convex on `s`, where `x, y ∈ s`,
+is convex on `Icc 0 1` (the segment from `x` to `y` lies in `s` by convexity of `s`). -/
+theorem ConvexOn.lineRestriction (hc : ConvexOn ℝ s f) (hx : x ∈ s) (hy : y ∈ s) :
+    ConvexOn ℝ (Set.Icc 0 1) (fun t : ℝ => f (x + t • (y - x))) := by
+  simpa only [Function.comp_def, lineMap_eq_add_smul_sub] using
+    (hc.comp_affineMap (AffineMap.lineMap x y)).subset
+      (fun t ht => hc.1.segment_subset hx hy (lineMap_mem_segment ℝ x y ht)) (convex_Icc _ _)
+
+/-- The 1D restriction `t ↦ f (x + t • (y - x))` of a function concave on `s`, where `x, y ∈ s`,
+is concave on `Icc 0 1`. -/
+theorem ConcaveOn.lineRestriction (hc : ConcaveOn ℝ s f) (hx : x ∈ s) (hy : y ∈ s) :
+    ConcaveOn ℝ (Set.Icc 0 1) (fun t : ℝ => f (x + t • (y - x))) := by
+  simpa [Pi.neg_def] using (hc.neg.lineRestriction hx hy).neg
+
+/-- The 1D restriction `t ↦ f (x + t • (y - x))` of a function strictly convex on `s`, with
+`x ≠ y` both in `s`, is strictly convex on `Icc 0 1`. -/
+theorem StrictConvexOn.lineRestriction (hc : StrictConvexOn ℝ s f) (hx : x ∈ s) (hy : y ∈ s)
+    (hxy : x ≠ y) :
+    StrictConvexOn ℝ (Set.Icc 0 1) (fun t : ℝ => f (x + t • (y - x))) := by
+  refine ⟨convex_Icc _ _, fun t₁ ht₁ t₂ ht₂ ht_ne a b ha hb hab => ?_⟩
+  have hmem : ∀ t ∈ Set.Icc (0 : ℝ) 1, x + t • (y - x) ∈ s := fun t ht =>
+    lineMap_eq_add_smul_sub x y t ▸ hc.1.segment_subset hx hy (lineMap_mem_segment ℝ x y ht)
+  have hp_ne : x + t₁ • (y - x) ≠ x + t₂ • (y - x) := fun h =>
+    ht_ne (smul_left_injective ℝ (sub_ne_zero.mpr hxy.symm) (add_left_cancel h))
+  simpa only [show a • (x + t₁ • (y - x)) + b • (x + t₂ • (y - x))
+        = x + (a • t₁ + b • t₂) • (y - x) by rw [show b = 1 - a by linarith]; module]
+    using hc.2 (hmem t₁ ht₁) (hmem t₂ ht₂) hp_ne ha hb hab
+
+/-- The 1D restriction `t ↦ f (x + t • (y - x))` of a function strictly concave on `s`, with
+`x ≠ y` both in `s`, is strictly concave on `Icc 0 1`. -/
+theorem StrictConcaveOn.lineRestriction (hc : StrictConcaveOn ℝ s f) (hx : x ∈ s) (hy : y ∈ s)
+    (hxy : x ≠ y) :
+    StrictConcaveOn ℝ (Set.Icc 0 1) (fun t : ℝ => f (x + t • (y - x))) := by
+  have hneg : StrictConvexOn ℝ (Set.Icc 0 1) (fun t : ℝ => -f (x + t • (y - x))) := by
+    simpa using hc.neg.lineRestriction hx hy hxy
+  simpa [Pi.neg_def] using hneg.neg
+
+namespace ConvexOn
+
+/-- For a convex function `f` with line derivative `f'` at `x` in direction `y - x`,
+the first-order inequality `f x + f' ≤ f y` holds. -/
+theorem add_hasLineDerivAt_le (hc : ConvexOn ℝ s f) (hx : x ∈ s) (hy : y ∈ s)
+    {f' : ℝ} (hf : HasLineDerivAt ℝ f f' x (y - x)) :
+    f x + f' ≤ f y := by
+  simpa using (hc.lineRestriction hx hy).add_hasDerivAt_mul_le
+    (Set.left_mem_Icc.mpr zero_le_one) (Set.right_mem_Icc.mpr zero_le_one)
+    zero_lt_one hf
+
+/-- For a convex function `f` line-differentiable at `x` in direction `y - x`,
+the first-order inequality `f x + lineDeriv ℝ f x (y - x) ≤ f y` holds. -/
+theorem add_lineDeriv_le (hc : ConvexOn ℝ s f) (hx : x ∈ s) (hy : y ∈ s)
+    (hf : LineDifferentiableAt ℝ f x (y - x)) :
+    f x + lineDeriv ℝ f x (y - x) ≤ f y :=
+  hc.add_hasLineDerivAt_le hx hy hf.hasLineDerivAt
+
+/-- Monotonicity of the directional derivative along the chord: for convex `f`
+line-differentiable at both endpoints in direction `y - x`,
+`0 ≤ lineDeriv ℝ f y (y - x) - lineDeriv ℝ f x (y - x)`. -/
+theorem lineDeriv_sub_nonneg (hc : ConvexOn ℝ s f) (hx : x ∈ s) (hy : y ∈ s)
+    (hfx : LineDifferentiableAt ℝ f x (y - x))
+    (hfy : LineDifferentiableAt ℝ f y (y - x)) :
+    0 ≤ lineDeriv ℝ f y (y - x) - lineDeriv ℝ f x (y - x) := by
+  have hfy' : LineDifferentiableAt ℝ f y (x - y) := by
+    simpa only [neg_one_smul, neg_sub] using hfy.smul (-1 : ℝ)
+  have h₂ : f y - lineDeriv ℝ f y (y - x) ≤ f x := by
+    simpa only [← neg_sub y x, lineDeriv_neg, ← sub_eq_add_neg]
+      using hc.add_lineDeriv_le hy hx hfy'
+  linarith [hc.add_lineDeriv_le hx hy hfx]
+
+end ConvexOn
+
+namespace ConcaveOn
+
+/-- For a concave function `f` with line derivative `f'` at `x` in direction `y - x`,
+the reverse first-order inequality `f y ≤ f x + f'` holds. -/
+theorem le_add_hasLineDerivAt (hc : ConcaveOn ℝ s f) (hx : x ∈ s) (hy : y ∈ s)
+    {f' : ℝ} (hf : HasLineDerivAt ℝ f f' x (y - x)) :
+    f y ≤ f x + f' := by
+  simpa using (hc.lineRestriction hx hy).le_add_hasDerivAt_mul
+    (Set.left_mem_Icc.mpr zero_le_one) (Set.right_mem_Icc.mpr zero_le_one)
+    zero_lt_one hf
+
+/-- For a concave function `f` line-differentiable at `x` in direction `y - x`,
+the reverse first-order inequality `f y ≤ f x + lineDeriv ℝ f x (y - x)` holds. -/
+theorem le_add_lineDeriv (hc : ConcaveOn ℝ s f) (hx : x ∈ s) (hy : y ∈ s)
+    (hf : LineDifferentiableAt ℝ f x (y - x)) :
+    f y ≤ f x + lineDeriv ℝ f x (y - x) :=
+  hc.le_add_hasLineDerivAt hx hy hf.hasLineDerivAt
+
+end ConcaveOn
+
+namespace StrictConvexOn
+
+/-- Strict variant of the first-order inequality for strictly convex `f` with line derivative
+`f'` at `x` in direction `y - x`, assuming `x ≠ y`: `f x + f' < f y`. -/
+theorem add_hasLineDerivAt_lt (hc : StrictConvexOn ℝ s f) (hx : x ∈ s) (hy : y ∈ s) (hxy : x ≠ y)
+    {f' : ℝ} (hf : HasLineDerivAt ℝ f f' x (y - x)) :
+    f x + f' < f y := by
+  simpa using (hc.lineRestriction hx hy hxy).add_hasDerivAt_mul_lt
+    (Set.left_mem_Icc.mpr zero_le_one) (Set.right_mem_Icc.mpr zero_le_one)
+    zero_lt_one hf
+
+/-- Strict variant of the first-order inequality for strictly convex `f`: when `x ≠ y` and `f`
+is line-differentiable at `x` in direction `y - x`, the inequality is strict. -/
+theorem add_lineDeriv_lt (hc : StrictConvexOn ℝ s f) (hx : x ∈ s) (hy : y ∈ s) (hxy : x ≠ y)
+    (hf : LineDifferentiableAt ℝ f x (y - x)) :
+    f x + lineDeriv ℝ f x (y - x) < f y :=
+  hc.add_hasLineDerivAt_lt hx hy hxy hf.hasLineDerivAt
+
+end StrictConvexOn
+
+namespace StrictConcaveOn
+
+/-- Strict variant of the reverse first-order inequality for strictly concave `f` with line
+derivative `f'` at `x` in direction `y - x`, assuming `x ≠ y`: `f y < f x + f'`. -/
+theorem lt_add_hasLineDerivAt (hc : StrictConcaveOn ℝ s f) (hx : x ∈ s) (hy : y ∈ s) (hxy : x ≠ y)
+    {f' : ℝ} (hf : HasLineDerivAt ℝ f f' x (y - x)) :
+    f y < f x + f' := by
+  simpa using (hc.lineRestriction hx hy hxy).lt_add_hasDerivAt_mul
+    (Set.left_mem_Icc.mpr zero_le_one) (Set.right_mem_Icc.mpr zero_le_one)
+    zero_lt_one hf
+
+/-- Strict variant of the reverse first-order inequality for strictly concave `f`: when `x ≠ y`
+and `f` is line-differentiable at `x` in direction `y - x`, the inequality is strict. -/
+theorem lt_add_lineDeriv (hc : StrictConcaveOn ℝ s f) (hx : x ∈ s) (hy : y ∈ s) (hxy : x ≠ y)
+    (hf : LineDifferentiableAt ℝ f x (y - x)) :
+    f y < f x + lineDeriv ℝ f x (y - x) :=
+  hc.lt_add_hasLineDerivAt hx hy hxy hf.hasLineDerivAt
+
+end StrictConcaveOn
diff --git a/Mathlib/MeasureTheory/Integral/CurveIntegral/Basic.lean b/Mathlib/MeasureTheory/Integral/CurveIntegral/Basic.lean
index dd62fc98ff3080..017b0680d8bd9b 100644
--- a/Mathlib/MeasureTheory/Integral/CurveIntegral/Basic.lean
+++ b/Mathlib/MeasureTheory/Integral/CurveIntegral/Basic.lean
@@ -11,6 +11,9 @@ public import Mathlib.Analysis.Calculus.Deriv.AffineMap
 public import Mathlib.Analysis.Calculus.Deriv.Shift
 public import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
 
+import Mathlib.Analysis.Calculus.AddTorsor.AffineMap
+import Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
+
 /-!
 # Integral of a 1-form along a path
 
@@ -286,20 +289,31 @@ theorem curveIntegral_trans (h₁ : CurveIntegrable ω γab) (h₂ : CurveIntegr
   simp only [curveIntegral_def]
   norm_num
 
-theorem curveIntegralFun_segment [NormedSpace ℝ E] (ω : E → E →L[𝕜] F) (a b : E)
-    {t : ℝ} (ht : t ∈ I) : curveIntegralFun ω (.segment a b) t = ω (lineMap a b t) (b - a) := by
+end PathOperations
+
+section Segment
+
+variable {𝕜 E F : Type*} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace ℝ E]
+  [NormedAddCommGroup F] [NormedSpace 𝕜 F] {a b c d : E} {ω : E → E →L[𝕜] F}
+  {γ γab : Path a b} {γbc : Path b c} {t : ℝ}
+
+theorem curveIntegralFun_segment (ω : E → E →L[𝕜] F) (a b : E) {t : ℝ} (ht : t ∈ I) :
+    curveIntegralFun ω (.segment a b) t = ω (lineMap a b t) (b - a) := by
   have := Path.eqOn_extend_segment a b
   simp only [curveIntegralFun_def, this ht, derivWithin_congr this (this ht),
     (hasDerivWithinAt_lineMap ..).derivWithin (uniqueDiffOn_Icc_zero_one t ht)]
 
-theorem curveIntegrable_segment [NormedSpace ℝ E] :
-    CurveIntegrable ω (.segment a b) ↔
+theorem curveIntegrable_segment : CurveIntegrable ω (.segment a b) ↔
       IntervalIntegrable (fun t ↦ ω (lineMap a b t) (b - a)) volume 0 1 := by
   rw [CurveIntegrable, intervalIntegrable_congr]
   rw [uIoc_of_le zero_le_one]
   exact .mono Ioc_subset_Icc_self fun _t ↦ curveIntegralFun_segment ω a b
 
-theorem curveIntegral_segment [NormedSpace ℝ E] [NormedSpace ℝ F] (ω : E → E →L[𝕜] F) (a b : E) :
+@[simp] theorem curveIntegrable_segment_const (ω : E →L[𝕜] F) (a b : E) :
+    CurveIntegrable (fun _ : E ↦ ω) (.segment a b) :=
+  curveIntegrable_segment.mpr intervalIntegrable_const
+
+theorem curveIntegral_segment [NormedSpace ℝ F] (ω : E → E →L[𝕜] F) (a b : E) :
     ∫ᶜ x in .segment a b, ω x = ∫ t in 0..1, ω (lineMap a b t) (b - a) := by
   rw [curveIntegral_def]
   refine intervalIntegral.integral_congr fun t ht ↦ ?_
@@ -307,14 +321,14 @@ theorem curveIntegral_segment [NormedSpace ℝ E] [NormedSpace ℝ F] (ω : E 
   exact curveIntegralFun_segment ω a b ht
 
 @[simp]
-theorem curveIntegral_segment_const [NormedSpace ℝ E] [CompleteSpace F] (ω : E →L[𝕜] F) (a b : E) :
+theorem curveIntegral_segment_const [CompleteSpace F] (ω : E →L[𝕜] F) (a b : E) :
     ∫ᶜ _ in .segment a b, ω = ω (b - a) := by
   letI : NormedSpace ℝ F := .restrictScalars ℝ 𝕜 F
   simp [curveIntegral_segment]
 
 /-- If `‖ω z‖ ≤ C` at all points of the segment `[a -[ℝ] b]`,
 then the curve integral `∫ᶜ x in .segment a b, ω x` has norm at most `C * ‖b - a‖`. -/
-theorem norm_curveIntegral_segment_le [NormedSpace ℝ E] {C : ℝ} (h : ∀ z ∈ [a -[ℝ] b], ‖ω z‖ ≤ C) :
+theorem norm_curveIntegral_segment_le {C : ℝ} (h : ∀ z ∈ [a -[ℝ] b], ‖ω z‖ ≤ C) :
     ‖∫ᶜ x in .segment a b, ω x‖ ≤ C * ‖b - a‖ := calc
   ‖∫ᶜ x in .segment a b, ω x‖ ≤ C * ‖b - a‖ * |1 - 0| := by
     letI : NormedSpace ℝ F := .restrictScalars ℝ 𝕜 F
@@ -325,18 +339,42 @@ theorem norm_curveIntegral_segment_le [NormedSpace ℝ E] {C : ℝ} (h : ∀ z 
     apply_rules [(ω _).le_of_opNorm_le, mem_image_of_mem, Ioc_subset_Icc_self]
   _ = C * ‖b - a‖ := by simp
 
-/-- If a 1-form `ω` is continuous on a set `s`,
-then it is curve integrable along any $C^1$ path in this set. -/
-theorem ContinuousOn.curveIntegrable_of_contDiffOn [NormedSpace ℝ E] {s : Set E}
-    (hω : ContinuousOn ω s) (hγ : ContDiffOn ℝ 1 γ.extend I) (hγs : ∀ t, γ t ∈ s) :
-    CurveIntegrable ω γ := by
+theorem ContinuousOn.curveIntegrable_of_contDiffOn {s : Set E} (hω : ContinuousOn ω s)
+    (hγ : ContDiffOn ℝ 1 γ.extend I) (hγs : ∀ t, γ t ∈ s) : CurveIntegrable ω γ := by
   apply ContinuousOn.intervalIntegrable_of_Icc zero_le_one
   simp only [funext (curveIntegralFun_def ω γ)]
   apply ContinuousOn.clm_apply
   · exact hω.comp (by fun_prop) fun _ _ ↦ hγs _
   · exact hγ.continuousOn_derivWithin uniqueDiffOn_Icc_zero_one le_rfl
 
-end PathOperations
+@[fun_prop]
+theorem Path.contDiffOn_segment_extend (a b : E) :
+    ContDiffOn ℝ 1 (Path.segment a b).extend I :=
+  (AffineMap.contDiff_lineMap a b).contDiffOn.congr (Path.eqOn_extend_segment a b)
+
+theorem ContinuousOn.curveIntegrable_segment (hω : ContinuousOn ω [a -[ℝ] b]) :
+    CurveIntegrable ω (.segment a b) :=
+  hω.curveIntegrable_of_contDiffOn (Path.contDiffOn_segment_extend a b)
+    fun t ↦ Path.range_segment a b ▸ Set.mem_range_self t
+
+theorem Continuous.curveIntegrable_segment (hω : Continuous ω) :
+    CurveIntegrable ω (.segment a b) := hω.continuousOn.curveIntegrable_segment
+
+/-- **Fundamental theorem of calculus along a line segment.** If `f : E → F` is differentiable
+on `[a -[ℝ] b]` and its derivative is continuous on the segment, then the curve integral of
+`fderiv ℝ f` along the segment equals `f b - f a`. -/
+theorem curveIntegral_fderiv_segment [NormedSpace ℝ F] [CompleteSpace F] {f : E → F}
+    (hf : ∀ z ∈ [a -[ℝ] b], DifferentiableAt ℝ f z)
+    (hcont : ContinuousOn (fderiv ℝ f) [a -[ℝ] b]) :
+    ∫ᶜ z in .segment a b, fderiv ℝ f z = f b - f a := by
+  rw [curveIntegral_segment]
+  simpa using intervalIntegral.integral_eq_sub_of_hasDerivAt
+    (fun t ht ↦ (hf _ (segment_eq_image_lineMap ℝ a b ▸ mem_image_of_mem _
+        (uIcc_of_le (zero_le_one : (0 : ℝ) ≤ 1) ▸ ht))).hasFDerivAt
+      |>.comp_hasDerivAt t AffineMap.hasDerivAt_lineMap)
+    (curveIntegrable_segment.mp hcont.curveIntegrable_segment)
+
+end Segment
 
 /-!
 ### Algebraic operations on the 1-form