refactor(Analysis/Convex): apply review feedback

Must-fixes (1)–(3):
- Add strict 1D additive forms `StrictConvexOn.add_hasDerivAt_mul_lt` and
  `StrictConcaveOn.lt_add_hasDerivAt_mul` (plus `deriv`-form variants) to
  `Convex/Deriv.lean`.
- Refactor `StrictConvexOn.add_lineDeriv_lt` to use the new strict 1D additive
  form via `StrictConvexOn.lineRestriction` (drops the brittle midpoint `calc`).
- Add `StrictConcaveOn.lt_add_lineDeriv`, `.lt_add_fderiv`, `.lt_add_inner_gradient`
  (missing concave strict duals across all three layers).
- Add `ConvexOn.isMinOn_of_fderiv_eq_zero` (FDeriv-form sibling of the gradient
  one; needs only `NormedSpace ℝ E`, not Hilbert).
- Add `HasLineDerivAt`- and `HasFDerivAt`-flavoured primitive forms for all
  inequality lemmas; the `lineDeriv` / `fderiv` versions become one-line
  corollaries via `LineDifferentiableAt.hasLineDerivAt` /
  `DifferentiableAt.hasFDerivAt`.

Should-fixes (4)–(7):
- Rename `_sub_apply_nonneg` → `_sub_nonneg` in both LineDeriv and FDeriv;
  `_apply` was vestigial for the scalar `lineDeriv` and added noise for
  `fderiv` where the application is visible in the statement.
- Drop the LineDeriv-layer iff converse (`convexOn_iff_add_lineDeriv_le`);
  the FDeriv-layer iff is the canonical statement users want, and its
  premise `∀ x ∈ s, DifferentiableAt ℝ f x` is easier to instantiate than
  the pair-quantified line-differentiability of the dropped version.
- Reprove `convexOn_iff_add_fderiv_le` directly using `fderiv`-arithmetic
  (no longer delegating through the dropped LineDeriv iff).
- Rewrite Gradient module docstring to lead with "Hilbert space" framing.
- Refactor the `▸` chain in `ConvexOn.lineDeriv_sub_nonneg` to a `have` +
  `rw` block.

Bonus: factor out `private lineMap_eq_add_smul_sub` helper.

Author: FordUniver

Mathlib/Analysis/Convex/Deriv.lean

@@ -790,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
@@ -1024,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

@@ -17,14 +17,22 @@ 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 `DifferentiableAt.lineDeriv_eq_fderiv`.
+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).
-* `ConcaveOn.le_add_fderiv` — the concave dual.
-* `ConvexOn.fderiv_sub_apply_nonneg` — monotonicity: `0 ≤ (fderiv ℝ f y - fderiv ℝ f x) (y - x)`.
-* `StrictConvexOn.add_fderiv_lt` — strict variant.
+* `ConvexOn.add_hasFDerivAt_le` / `ConvexOn.add_fderiv_le` — the first-order convexity
+  inequality (Fréchet form).
+* `ConcaveOn.le_add_hasFDerivAt` / `ConcaveOn.le_add_fderiv` — the concave dual.
+* `ConvexOn.fderiv_sub_nonneg` — monotonicity along the chord:
+  `0 ≤ (fderiv ℝ f y - fderiv ℝ f x) (y - x)`.
+* `StrictConvexOn.add_hasFDerivAt_lt` / `StrictConvexOn.add_fderiv_lt` — strict variant.
+* `StrictConcaveOn.lt_add_hasFDerivAt` / `StrictConcaveOn.lt_add_fderiv` — strict concave dual.
+* `ConvexOn.isMinOn_of_fderiv_eq_zero` — convex + zero Fréchet derivative at `x` ⟹ `x`
+  minimises `f`.
 * `convexOn_iff_add_fderiv_le` — iff converse: differentiability plus the first-order
   inequality everywhere implies `ConvexOn`.
 -/
@@ -36,51 +44,114 @@ 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 :=
-  hf.lineDeriv_eq_fderiv ▸ hc.add_lineDeriv_le hx hy hf.lineDifferentiableAt
+  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_apply_nonneg (hc : ConvexOn ℝ s f) (hx : x ∈ s) (hy : y ∈ s)
+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 [ContinuousLinearMap.sub_apply, ← hfx.lineDeriv_eq_fderiv, ← hfy.lineDeriv_eq_fderiv]
-  exact hc.lineDeriv_sub_apply_nonneg hx hy hfx.lineDifferentiableAt hfy.lineDifferentiableAt
+  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) :=
-  hf.lineDeriv_eq_fderiv ▸ hc.le_add_lineDeriv hx hy hf.lineDifferentiableAt
+  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 :=
-  hf.lineDeriv_eq_fderiv ▸ hc.add_lineDeriv_lt hx hy hxy hf.lineDifferentiableAt
+  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
-  rw [convexOn_iff_add_lineDeriv_le hs fun x hx _ _ => (hf x hx).lineDifferentiableAt]
-  refine forall_congr' fun x => imp_congr_right fun hx => forall_congr' fun _ =>
-    imp_congr_right fun _ => ?_
-  rw [(hf x hx).lineDeriv_eq_fderiv]
+  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) with hL
+  change f z ≤ a • f x + b • f y
+  simp only [smul_eq_mul]
+  have hzs : z ∈ s := hs hx hy ha hb hab
+  have hb_eq : b = 1 - a := by linarith
+  have hxz : x - z = b • (x - y) := by rw [hz, hb_eq]; module
+  have hyz : y - z = -(a • (x - y)) := by rw [hz, hb_eq]; module
+  have hzx : f z + b * L ≤ f x := by
+    have h := H z hzs x hx
+    rwa [hxz, (fderiv ℝ f z).map_smul, smul_eq_mul] at h
+  have hzy : f z - a * L ≤ f y := by
+    have h := H z hzs y hy
+    rw [hyz, map_neg, (fderiv ℝ f z).map_smul, smul_eq_mul] at h
+    linarith
+  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

@@ -11,21 +11,24 @@ public import Mathlib.Analysis.Calculus.Gradient.Basic
 /-!
 # First-order convexity inequality via the gradient
 
-For `f : F → ℝ` convex on `s ⊆ F` on a Hilbert space and differentiable at `x ∈ s`,
+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 `inner_gradient_left`.
+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).
 * `ConcaveOn.le_add_inner_gradient` — the concave dual.
-* `ConvexOn.inner_gradient_sub_nonneg` — monotonicity: `0 ≤ ⟪∇ f y - ∇ f x, y - x⟫`.
-* `ConvexOn.isMinOn_of_gradient_eq_zero` — convex + zero gradient at `x` ⟹ `x` minimizes `f`.
+* `ConvexOn.inner_gradient_sub_nonneg` — monotonicity along the chord:
+  `0 ≤ ⟪∇ f y - ∇ f x, y - x⟫`.
+* `ConvexOn.isMinOn_of_gradient_eq_zero` — convex + zero gradient at `x` ⟹ `x` minimises `f`.
 * `StrictConvexOn.add_inner_gradient_lt` — strict variant.
+* `StrictConcaveOn.lt_add_inner_gradient` — strict concave dual.
 * `convexOn_iff_add_inner_gradient_le` — iff converse.
 -/
 
@@ -54,7 +57,7 @@ theorem inner_gradient_sub_nonneg (hc : ConvexOn ℝ s f) (hx : x ∈ s) (hy : y
     0 ≤ ⟪∇ f y - ∇ f x, y - x⟫ := by
   rw [inner_sub_left, inner_gradient_left, inner_gradient_left,
     ← ContinuousLinearMap.sub_apply]
-  exact hc.fderiv_sub_apply_nonneg hx hy hfx hfy
+  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`.
@@ -89,6 +92,17 @@ theorem add_inner_gradient_lt (hc : StrictConvexOn ℝ s f) (hx : x ∈ s) (hy :
 
 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)