feat(Analysis/Convex): first-order convexity inequalities

Mathlib.lean

@@ -1951,17 +1951,20 @@ 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
 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

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

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)

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]