diff --git a/Mathlib.lean b/Mathlib.lean
index 25322c6b37cb10..4c02e90fdc611e 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -1951,10 +1951,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 +1964,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/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