diff --git a/LeanMachineLearning.lean b/LeanMachineLearning.lean
index 3d683931..ef058a9c 100644
--- a/LeanMachineLearning.lean
+++ b/LeanMachineLearning.lean
@@ -1,5 +1,8 @@
 module  -- shake: keep-all --deprecated_module: ignore
 
+public import LeanMachineLearning.ForMathlib.Analysis.Convex.Bregman.Basic
+public import LeanMachineLearning.ForMathlib.Analysis.Convex.Subgradient.Basic
+public import LeanMachineLearning.ForMathlib.Analysis.Convex.Subgradient.Deriv
 public import LeanMachineLearning.ForMathlib.InformationTheory.KullbackLeibler.ChainRule
 public import LeanMachineLearning.ForMathlib.InformationTheory.KullbackLeibler.CompProd
 public import LeanMachineLearning.ForMathlib.InformationTheory.KullbackLeibler.Convex
diff --git a/LeanMachineLearning/ForMathlib/Analysis/Convex/Bregman/Basic.lean b/LeanMachineLearning/ForMathlib/Analysis/Convex/Bregman/Basic.lean
new file mode 100644
index 00000000..f73a2349
--- /dev/null
+++ b/LeanMachineLearning/ForMathlib/Analysis/Convex/Bregman/Basic.lean
@@ -0,0 +1,201 @@
+/-
+Copyright (c) 2026 Isidoor Pinillo Esquivel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Isidoor Pinillo Esquivel
+-/
+module
+
+public import Mathlib.Analysis.Convex.Function
+public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
+
+/-!
+# Bregman Divergences
+
+Generalized vector-valued Bregman divergences `bregDiv f x y J` (notation: `D_[f](x, y, J)`
+in `scoped Bregman`) measure the error of the linear approximation of `f` around `y`.
+They satisfy algebraic properties linked to derivatives, including chain rules,
+product rules, affine invariance, and convexity preservation.
+
+## Main definitions
+
+* `bregDiv f x y J`: The generalized vector-valued Bregman divergence `f x - f y - J (x - y)`
+  for a function `f : E → F` and a continuous linear map `J : E →L[R] F`
+  (e.g. a derivative, gradient, or subgradient).
+
+## Notation
+
+* `D_[f](x, y, J)`: Scoped notation in `Bregman` for `bregDiv f x y J`.
+-/
+
+@[expose] public section
+
+variable {R E E₁ E₂ F G : Type*} [Ring R]
+  [AddCommGroup E] [Module R E] [TopologicalSpace E]
+  [AddCommGroup E₁] [Module R E₁] [TopologicalSpace E₁]
+  [AddCommGroup E₂] [Module R E₂] [TopologicalSpace E₂]
+  [AddCommGroup F] [Module R F] [TopologicalSpace F]
+  [AddCommGroup G] [Module R G] [TopologicalSpace G]
+  {f : E → F} {x y z : E} {J J₁ J₂ J_x J_y : E →L[R] F}
+
+/-- The generalized vector-valued Bregman divergence.
+`f` maps `E → F`. `J` is the Jacobian / subgradient continuous linear mapping `E →L[R] F`. -/
+def bregDiv (f : E → F) (x y : E) (J : E →L[R] F) : F :=
+  f x - f y - J (x - y)
+
+/-- Scoped notation for `bregDiv`. -/
+scoped[Bregman] notation "D_[" f "](" x ", " y ", " J ")" => bregDiv f x y J
+
+open scoped Bregman
+
+@[simp]
+lemma bregDiv_self :
+    D_[f](x, x, J_x) = 0 := by
+  simp [bregDiv]
+
+lemma bregDiv_three_point [IsTopologicalAddGroup F] :
+    D_[f](z, x, J_x) + D_[f](x, y, J_y) - D_[f](z, y, J_y) = (J_y - J_x) (z - x) := by
+  simp only [bregDiv, map_sub, sub_apply]
+  abel
+
+lemma bregDiv_add_swap [IsTopologicalAddGroup F] :
+    D_[f](y, x, J_x) + D_[f](x, y, J_y) = (J_x - J_y) (x - y) := by
+  simp only [bregDiv, map_sub, sub_apply]
+  abel
+
+lemma bregDiv_fun_bregDiv [IsTopologicalAddGroup F] :
+    D_[fun w ↦ D_[f](w, y, J_y)](z, x, J_x - J_y) = D_[f](z, x, J_x) := by
+  simp only [bregDiv, map_sub, sub_apply]
+  abel
+
+@[to_fun]
+lemma bregDiv_add [ContinuousAdd F] (f₁ f₂ : E → F) :
+    D_[f₁ + f₂](x, y, J₁ + J₂) = D_[f₁](x, y, J₁) + D_[f₂](x, y, J₂) := by
+  simp only [bregDiv, Pi.add_apply, add_apply, map_sub]
+  abel
+
+lemma bregDiv_prod [ContinuousAdd F]
+    (f₁ : E₁ → F) (f₂ : E₂ → F) (x y : E₁ × E₂) (J₁ : E₁ →L[R] F) (J₂ : E₂ →L[R] F) :
+    D_[fun p : E₁ × E₂ ↦ f₁ p.1 + f₂ p.2](x, y, J₁.coprod J₂) =
+      D_[f₁](x.1, y.1, J₁) + D_[f₂](x.2, y.2, J₂) := by
+  simp only [bregDiv, ContinuousLinearMap.coprod_apply, map_sub]
+  abel
+
+@[simp]
+lemma bregDiv_const (c : F) :
+    D_[fun _ ↦ c](x, y, (0 : E →L[R] F)) = 0 := by
+  simp [bregDiv]
+
+@[simp]
+lemma bregDiv_linear (h : E →L[R] F) :
+    D_[h](x, y, h) = 0 := by
+  simp [bregDiv]
+
+@[simp]
+lemma bregDiv_add_const (c : F) :
+    D_[fun z ↦ f z + c](x, y, J) = D_[f](x, y, J) := by
+  simp [bregDiv]
+
+@[simp]
+lemma bregDiv_const_add (c : F) :
+    D_[fun z ↦ c + f z](x, y, J) = D_[f](x, y, J) := by
+  simp [bregDiv]
+
+@[simp]
+lemma bregDiv_add_linear [ContinuousAdd F] (h : E →L[R] F) :
+    D_[fun z ↦ f z + h z](x, y, J + h) = D_[f](x, y, J) := by
+  simp only [bregDiv, add_apply, map_sub]
+  abel
+
+@[to_fun (attr := simp)]
+lemma bregDiv_neg [IsTopologicalAddGroup F] :
+    D_[-f](x, y, -J) = - D_[f](x, y, J) := by
+  simp only [bregDiv, Pi.neg_apply, neg_apply, map_sub]
+  abel
+
+lemma bregDiv_comp_neg [IsTopologicalAddGroup F] :
+    D_[fun z ↦ f (-z)](x, y, -J) = D_[f](-x, -y, J) := by
+  simp [bregDiv, map_sub]
+
+lemma bregDiv_comp_add_right (x₀ : E) :
+    D_[fun z ↦ f (z + x₀)](x, y, J) = D_[f](x + x₀, y + x₀, J) := by
+  simp [bregDiv]
+
+section ChainRules
+
+variable {f₁ : E → F} {f₂ : F → G} {J₁ : E →L[R] F} {J₂ : F →L[R] G}
+  {A : E₁ →L[R] E} {b : E} {x y : E₁}
+
+lemma bregDiv_comp_affine :
+    D_[fun z ↦ f (A z + b)](x, y, J.comp A) = D_[f](A x + b, A y + b, J) := by
+  simp [bregDiv]
+
+lemma bregDiv_comp {x y : E} :
+    D_[f₂ ∘ f₁](x, y, J₂.comp J₁) = D_[f₂](f₁ x, f₁ y, J₂) + J₂ (D_[f₁](x, y, J₁)) := by
+  simp [bregDiv]
+
+end ChainRules
+
+section CommRing
+
+variable {R' : Type*} [CommRing R'] [TopologicalSpace R'] [ContinuousAdd R']
+  [ContinuousConstSMul R' R'] [Module R' E]
+
+/-- First-order product rule for Bregman divergences. -/
+@[to_fun]
+lemma bregDiv_mul (f₁ f₂ : E → R') (x y : E) (J₁ J₂ : E →L[R'] R') :
+    D_[f₁ * f₂](x, y, f₂ y • J₁ + f₁ y • J₂) =
+      D_[f₁](x, y, J₁) * f₂ y + f₁ y * D_[f₂](x, y, J₂) +
+      (f₁ x - f₁ y) * (f₂ x - f₂ y) := by
+  dsimp only [bregDiv]
+  simp only [Pi.mul_apply, add_apply, smul_apply, map_sub, smul_eq_mul]
+  ring
+
+end CommRing
+
+section Order
+
+variable {F' : Type*} [AddCommGroup F'] [Module R F'] [TopologicalSpace F']
+  [Preorder F'] [AddRightMono F']
+
+lemma bregDiv_le_of_le_of_eq {f₁ f₂ : E → F'} {x y : E} {J_y : E →L[R] F'}
+    (h_le : f₁ x ≤ f₂ x) (h_eq : f₁ y = f₂ y) :
+    D_[f₁](x, y, J_y) ≤ D_[f₂](x, y, J_y) := by
+  simp [bregDiv, h_eq, h_le]
+
+end Order
+
+section Module
+
+variable {R' : Type*} [CommRing R'] [Module R' E] [Module R' F] [ContinuousConstSMul R' F]
+
+lemma bregDiv_smul (c : R') (f : E → F) (x y : E) (J : E →L[R'] F) :
+    D_[c • f](x, y, c • J) = c • D_[f](x, y, J) := by
+  simp [bregDiv, smul_sub]
+
+lemma bregDiv_convexCombination [ContinuousAdd F]
+    (f : E → F) (x y : E) (J₁ J₂ : E →L[R'] F) {a b : R'} (hab : a + b = 1) :
+    D_[f](x, y, a • J₁ + b • J₂) = a • D_[f](x, y, J₁) + b • D_[f](x, y, J₂) := by
+  calc D_[f](x, y, a • J₁ + b • J₂)
+  _ = D_[(a + b) • f](x, y, a • J₁ + b • J₂) := by rw [hab, one_smul]
+  _ = D_[a • f](x, y, a • J₁) + D_[b • f](x, y, b • J₂) := by rw [add_smul, bregDiv_add]
+  _ = a • D_[f](x, y, J₁) + b • D_[f](x, y, J₂) := by simp only [bregDiv_smul]
+
+end Module
+
+section Convexity
+
+variable [PartialOrder R] [PartialOrder F] [IsOrderedAddMonoid F]
+
+/-- If `f` is convex on `s`, then `x ↦ D_[f](x, y, J)` is convex on `s` for any
+continuous linear map `J`. -/
+nonrec lemma ConvexOn.bregDiv {s : Set E} (hf : ConvexOn R s f) (J : E →L[R] F) (y : E) :
+    ConvexOn R s (fun x ↦ D_[f](x, y, J)) := by
+  simp only [bregDiv, sub_eq_add_neg, map_add, map_neg, neg_add_rev, neg_neg]
+  apply ConvexOn.add
+  · apply hf.add
+    exact convexOn_const (-f y) hf.1
+  · apply ConvexOn.add
+    · exact convexOn_const (J y) hf.1
+    · exact (-J.toLinearMap).convexOn hf.1
+
+end Convexity
diff --git a/LeanMachineLearning/ForMathlib/Analysis/Convex/Subgradient/Basic.lean b/LeanMachineLearning/ForMathlib/Analysis/Convex/Subgradient/Basic.lean
new file mode 100644
index 00000000..578da360
--- /dev/null
+++ b/LeanMachineLearning/ForMathlib/Analysis/Convex/Subgradient/Basic.lean
@@ -0,0 +1,240 @@
+/-
+Copyright (c) 2026 Isidoor Pinillo Esquivel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Isidoor Pinillo Esquivel
+-/
+module
+
+public import LeanMachineLearning.ForMathlib.Analysis.Convex.Bregman.Basic
+
+/-!
+# Subgradients and Subdifferentials
+
+Subgradients of functions `f : E → F` defined
+via the non-negativity of the Bregman divergence `0 ≤ D_[f](y, x, g)` on an explicit
+domain `s` (i.e. the linearization error is non-negative on `s`).
+
+Carrying the domain `s : Set E` explicitly avoids using indicator functions
+while supporting constrained convex analysis.
+
+## Main definitions
+
+* `HasSubgradientWithinAt f g s x`: `g : E →L[R] F` is a subgradient of `f` at `x` on `s`.
+* `subdifferentialWithin R f s x`: The subdifferential set `∂[R, s, x](f)`.
+
+## Main results
+
+* Monotonicity in the domain: `HasSubgradientWithinAt.mono`.
+* Chain rules: `HasSubgradientWithinAt.comp_affine` and `HasSubgradientWithinAt.comp`.
+* Equivalence with classical inequality: `hasSubgradientWithinAt_iff_le`.
+* Fermat's rule: `hasSubgradientWithinAt_zero_iff_isMinOn`.
+* Suprema and maxima: `HasSubgradientWithinAt.sup_left`, `HasSubgradientWithinAt.sup_right`,
+  `HasSubgradientWithinAt.finset_sup'`, and `HasSubgradientWithinAt.ciSup`.
+
+## Notation
+
+* `∂[R, s, x](f)`: Scoped notation in `Bregman` for `subdifferentialWithin R f s x`.
+-/
+
+@[expose] public section
+
+open scoped Bregman
+
+variable {R E E₁ F G : Type*} [Ring R]
+  [AddCommGroup E] [Module R E] [TopologicalSpace E]
+  [AddCommGroup E₁] [Module R E₁] [TopologicalSpace E₁]
+  [AddCommGroup F] [Module R F] [TopologicalSpace F]
+  [AddCommGroup G] [Module R G] [TopologicalSpace G]
+  [Preorder F]
+
+/-- `g` is a subgradient of `f` at `x` on domain `s` (non-negativity of Bregman divergence). -/
+def HasSubgradientWithinAt (f : E → F) (g : E →L[R] F) (s : Set E) (x : E) : Prop :=
+  ∀ y ∈ s, 0 ≤ D_[f](y, x, g)
+
+variable (R) in
+/-- The subdifferential `∂[R, s, x](f)` of `f` at `x` on `s`. -/
+def subdifferentialWithin (f : E → F) (s : Set E) (x : E) : Set (E →L[R] F) :=
+  { g | HasSubgradientWithinAt f g s x }
+
+/-- Scoped notation for `subdifferentialWithin`. -/
+scoped[Bregman] notation "∂[" R ", " s ", " x "](" f ")" => subdifferentialWithin R f s x
+
+variable {s t : Set E} {f : E → F} {x y : E} {g : E →L[R] F}
+
+@[simp]
+lemma mem_subdifferentialWithin :
+    g ∈ ∂[R, s, x](f) ↔ HasSubgradientWithinAt f g s x := Iff.rfl
+
+lemma HasSubgradientWithinAt.mono
+    (h : HasSubgradientWithinAt f g t x) (hst : s ⊆ t) :
+    HasSubgradientWithinAt f g s x :=
+  fun y hy ↦ h y (hst hy)
+
+@[simp]
+lemma hasSubgradientWithinAt_const (c : F) :
+    HasSubgradientWithinAt (fun _ ↦ c) (0 : E →L[R] F) s x := by
+  simp [HasSubgradientWithinAt]
+
+@[simp]
+lemma hasSubgradientWithinAt_linear (h : E →L[R] F) :
+    HasSubgradientWithinAt h h s x := by
+  simp [HasSubgradientWithinAt]
+
+@[simp]
+lemma hasSubgradientWithinAt_add_const_iff {c : F} :
+    HasSubgradientWithinAt (fun y ↦ f y + c) g s x ↔ HasSubgradientWithinAt f g s x := by
+  simp [HasSubgradientWithinAt, bregDiv]
+
+@[simp]
+lemma hasSubgradientWithinAt_const_add_iff {c : F} :
+    HasSubgradientWithinAt (fun y ↦ c + f y) g s x ↔ HasSubgradientWithinAt f g s x := by
+  simp [HasSubgradientWithinAt, bregDiv]
+
+@[simp]
+lemma hasSubgradientWithinAt_add_linear_iff [ContinuousAdd F] {h : E →L[R] F} :
+    HasSubgradientWithinAt (fun y ↦ f y + h y) (g + h) s x ↔ HasSubgradientWithinAt f g s x := by
+  simp [HasSubgradientWithinAt, bregDiv_add_linear]
+
+@[simp]
+lemma hasSubgradientWithinAt_bregDiv_iff [IsTopologicalAddGroup F] {g_x g_y : E →L[R] F} :
+    HasSubgradientWithinAt (fun z ↦ D_[f](z, y, g_y)) (g_x - g_y) s x ↔
+      HasSubgradientWithinAt f g_x s x := by
+  simp [HasSubgradientWithinAt, bregDiv_fun_bregDiv]
+
+lemma hasSubgradientWithinAt_zero_iff :
+    HasSubgradientWithinAt f (0 : E →L[R] F) s x ↔ ∀ y ∈ s, 0 ≤ f y - f x := by
+  simp [HasSubgradientWithinAt, bregDiv]
+
+lemma HasSubgradientWithinAt.comp_affine
+    {s₁ : Set E₁} {x₁ : E₁} {A : E₁ →L[R] E} {b : E}
+    (h_map : ∀ y ∈ s₁, A y + b ∈ s)
+    (h_sub : HasSubgradientWithinAt f g s (A x₁ + b)) :
+    HasSubgradientWithinAt (fun y ↦ f (A y + b)) (g.comp A) s₁ x₁ := fun y hy ↦ by
+  rw [bregDiv_comp_affine]
+  exact h_sub (A y + b) (h_map y hy)
+
+/-- **Chain rule**: `g₂ ∘ g₁` is a subgradient of `f₂ ∘ f₁` when `g₂` is monotone. -/
+lemma HasSubgradientWithinAt.comp [Preorder G] [IsOrderedAddMonoid G]
+    {f₂ : F → G} {f₁ : E → F} {g₂ : F →L[R] G} {g₁ : E →L[R] F}
+    (h₂ : HasSubgradientWithinAt f₂ g₂ (f₁ '' s) (f₁ x)) (h₁ : HasSubgradientWithinAt f₁ g₁ s x)
+    (hg₂ : Monotone g₂) :
+    HasSubgradientWithinAt (f₂ ∘ f₁) (g₂.comp g₁) s x := fun y hy ↦ by
+  rw [bregDiv_comp]
+  exact add_nonneg (h₂ (f₁ y) ⟨y, hy, rfl⟩) (by grw [← hg₂ (h₁ y hy)]; simp)
+
+section OrderedGroup
+
+variable [IsOrderedAddMonoid F]
+
+/-- Equivalence with the classical definition. -/
+lemma hasSubgradientWithinAt_iff_le :
+    HasSubgradientWithinAt f g s x ↔ ∀ y ∈ s, f x + g (y - x) ≤ f y := by
+  simp [HasSubgradientWithinAt, bregDiv, sub_sub, sub_nonneg]
+
+lemma HasSubgradientWithinAt.sub_apply_sub_nonneg [IsTopologicalAddGroup F] {g_x g_y : E →L[R] F}
+    (hx : x ∈ s) (hy : y ∈ s)
+    (hx_sub : HasSubgradientWithinAt f g_x s x) (hy_sub : HasSubgradientWithinAt f g_y s y) :
+    0 ≤ (g_x - g_y) (x - y) := by
+  rw [← bregDiv_add_swap]
+  exact add_nonneg (hx_sub y hy) (hy_sub x hx)
+
+lemma hasSubgradientWithinAt_zero_iff_isMinOn :
+    HasSubgradientWithinAt f (0 : E →L[R] F) s x ↔ IsMinOn f s x := by
+  simp [HasSubgradientWithinAt, bregDiv, sub_nonneg, isMinOn_iff]
+
+@[to_fun]
+lemma HasSubgradientWithinAt.add [ContinuousAdd F] {f₁ f₂ : E → F} {g₁ g₂ : E →L[R] F}
+    (h₁ : HasSubgradientWithinAt f₁ g₁ s x) (h₂ : HasSubgradientWithinAt f₂ g₂ s x) :
+    HasSubgradientWithinAt (f₁ + f₂) (g₁ + g₂) s x := fun y hy ↦ by
+  rw [bregDiv_add]
+  exact add_nonneg (h₁ y hy) (h₂ y hy)
+
+@[to_fun]
+lemma HasSubgradientWithinAt.add_isMinOn [ContinuousAdd F] {f₁ f₂ : E → F} {x : E} {g : E →L[R] F}
+    (h_min : IsMinOn f₁ s x) (h_sub : HasSubgradientWithinAt f₂ g s x) :
+    HasSubgradientWithinAt (f₁ + f₂) g s x := by
+  simpa using (hasSubgradientWithinAt_zero_iff_isMinOn.mpr h_min).add h_sub
+
+end OrderedGroup
+
+lemma HasSubgradientWithinAt.of_le_of_eq [AddRightMono F] {f₁ f₂ : E → F} {g : E →L[R] F}
+    (h_sub : HasSubgradientWithinAt f₁ g s x) (h_le : ∀ y ∈ s, f₁ y ≤ f₂ y) (h_eq : f₁ x = f₂ x) :
+    HasSubgradientWithinAt f₂ g s x :=
+  fun y hy ↦ le_trans (h_sub y hy)
+    (bregDiv_le_of_le_of_eq (h_le y hy) h_eq)
+
+section ModuleBasic
+
+variable {R' : Type*} [CommRing R'] [PartialOrder R']
+  [Module R' E] [Module R' F] [ContinuousConstSMul R' F] [PosSMulMono R' F]
+
+@[to_fun]
+lemma HasSubgradientWithinAt.smul {c : R'} (hc : 0 ≤ c) {f : E → F} {g : E →L[R'] F}
+    (h_sub : HasSubgradientWithinAt f g s x) :
+    HasSubgradientWithinAt (c • f) (c • g) s x := fun y hy ↦ by
+  rw [bregDiv_smul]
+  exact smul_nonneg hc (h_sub y hy)
+
+end ModuleBasic
+
+section Module
+
+variable {R' : Type*} [CommRing R'] [PartialOrder R']
+    [Module R' E] [IsOrderedAddMonoid F] [Module R' F] [ContinuousConstSMul R' F] [PosSMulMono R' F]
+    [ContinuousAdd F]
+
+lemma HasSubgradientWithinAt.convexCombination {f : E → F} {g₁ g₂ : E →L[R'] F}
+    (h₁ : HasSubgradientWithinAt f g₁ s x) (h₂ : HasSubgradientWithinAt f g₂ s x)
+    {a b : R'} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) :
+    HasSubgradientWithinAt f (a • g₁ + b • g₂) s x := fun y hy ↦ by
+  rw [bregDiv_convexCombination _ _ _ _ _ hab]
+  exact add_nonneg (smul_nonneg ha (h₁ y hy)) (smul_nonneg hb (h₂ y hy))
+
+lemma convex_subdifferentialWithin : Convex R' (∂[R', s, x](f)) := by
+  intro g₁ hg₁ g₂ hg₂ a b ha hb hab
+  simp only [mem_subdifferentialWithin] at hg₁ hg₂ ⊢
+  exact hg₁.convexCombination hg₂ ha hb hab
+
+end Module
+
+section SemilatticeSup
+
+variable {F_lin : Type*} [AddCommGroup F_lin] [Module R F_lin] [TopologicalSpace F_lin]
+  [SemilatticeSup F_lin] [IsOrderedAddMonoid F_lin]
+
+@[to_fun]
+lemma HasSubgradientWithinAt.sup_left {f₁ f₂ : E → F_lin} {g : E →L[R] F_lin}
+    (h_sub : HasSubgradientWithinAt f₁ g s x) (h_active : f₂ x ≤ f₁ x) :
+    HasSubgradientWithinAt (f₁ ⊔ f₂) g s x :=
+  h_sub.of_le_of_eq (fun y _ ↦ le_sup_left) (by simpa)
+
+@[to_fun]
+lemma HasSubgradientWithinAt.sup_right {f₁ f₂ : E → F_lin} {g : E →L[R] F_lin}
+    (h_sub : HasSubgradientWithinAt f₂ g s x) (h_active : f₁ x ≤ f₂ x) :
+    HasSubgradientWithinAt (f₁ ⊔ f₂) g s x :=
+  h_sub.of_le_of_eq (fun y _ ↦ le_sup_right) (by simpa)
+
+lemma HasSubgradientWithinAt.finset_sup' {ι : Type*} {s_ι : Finset ι}
+    {f_i : ι → E → F_lin} {i : ι} {g : E →L[R] F_lin}
+    (his : i ∈ s_ι)
+    (h_sub : HasSubgradientWithinAt (f_i i) g s x)
+    (h_active : ∀ j ∈ s_ι, f_i j x ≤ f_i i x) :
+    HasSubgradientWithinAt (fun y ↦ s_ι.sup' ⟨i, his⟩ (f_i · y)) g s x := by
+  refine h_sub.of_le_of_eq (fun _ _ ↦ Finset.le_sup'_of_le _ his le_rfl) ?_
+  exact le_antisymm (Finset.le_sup' (f := fun j => f_i j x) his) (Finset.sup'_le _ _ h_active)
+
+end SemilatticeSup
+
+section Lattice
+
+variable {F_lat : Type*} [AddCommGroup F_lat] [Module R F_lat] [TopologicalSpace F_lat]
+    [ConditionallyCompleteLattice F_lat] [IsOrderedAddMonoid F_lat]
+
+lemma HasSubgradientWithinAt.ciSup {ι : Type*} {f_i : ι → E → F_lat} {i : ι} {g : E →L[R] F_lat}
+    (h_sub : HasSubgradientWithinAt (f_i i) g s x)
+    (h_active : f_i i x = ⨆ j, f_i j x)
+    (h_bdd : ∀ y ∈ s, BddAbove (Set.range (f_i · y))) :
+    HasSubgradientWithinAt (fun y ↦ ⨆ j, f_i j y) g s x :=
+  h_sub.of_le_of_eq (fun y hy ↦ le_ciSup (h_bdd y hy) i) h_active
+
+end Lattice
diff --git a/LeanMachineLearning/ForMathlib/Analysis/Convex/Subgradient/Deriv.lean b/LeanMachineLearning/ForMathlib/Analysis/Convex/Subgradient/Deriv.lean
new file mode 100644
index 00000000..8510abad
--- /dev/null
+++ b/LeanMachineLearning/ForMathlib/Analysis/Convex/Subgradient/Deriv.lean
@@ -0,0 +1,168 @@
+/-
+Copyright (c) 2026 Isidoor Pinillo Esquivel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Isidoor Pinillo Esquivel
+-/
+module
+
+public import LeanMachineLearning.ForMathlib.Analysis.Convex.Subgradient.Basic
+public import Mathlib.Analysis.Calculus.LineDeriv.Basic
+
+/-!
+# Fréchet Derivatives and Subgradients
+
+This file establishes the connection between Fréchet derivatives (`HasFDerivWithinAt`,
+`HasFDerivAt`) and subgradients (`HasSubgradientWithinAt f g s x`) for convex functions.
+
+## Main results
+
+* `HasFDerivWithinAt.hasSubgradientWithinAt`: A Fréchet derivative within `s` of a function convex
+  on `s` is a subgradient on `s`. `HasFDerivAt.hasSubgradientWithinAt` is the special case of a
+  derivative at a point.
+* `HasFDerivAt.eq_of_hasSubgradientWithinAt`: Uniqueness of the subgradient at an interior
+  differentiable point.
+* `HasFDerivAt.subdifferentialWithin_add`: Subdifferential sum rule when one component is
+  Fréchet differentiable.
+-/
+
+@[expose] public section
+
+variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
+variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
+variable {f : E → F} {s : Set E} {x : E} {g h : E →L[ℝ] F}
+
+open scoped Bregman Topology Pointwise
+open Filter
+
+/-- As `t → 0` along the steps `t` with `x + t • w ∈ s`, the linearization error of a function
+Fréchet differentiable within `s` scaled by `t⁻¹` converges to `0`. -/
+lemma HasFDerivWithinAt.tendsto_bregDiv_slope_zero
+    (hderiv : HasFDerivWithinAt f g s x) (w : E) :
+    Tendsto (fun t : ℝ ↦ t⁻¹ • D_[f](x + t • w, x, g))
+      (𝓝[(fun t : ℝ ↦ x + t • w) ⁻¹' s \ {0}] 0) (𝓝 0) := by
+  have h := (hasDerivWithinAt_iff_tendsto_slope.mp (hderiv.hasLineDerivWithinAt w)).sub_const (g w)
+  rw [sub_self] at h
+  refine h.congr' ?_
+  filter_upwards [self_mem_nhdsWithin] with t ht
+  have ht0 : t ≠ 0 := ht.2
+  simp [bregDiv, slope, smul_sub, ht0]
+
+/-- As the step size `t → 0⁺`, the linearization error of a Fréchet differentiable function
+scaled by `t⁻¹` converges to `0`. -/
+lemma HasFDerivAt.tendsto_bregDiv_slope_zero
+    (hderiv : HasFDerivAt f g x) (w : E) :
+    Tendsto (fun t : ℝ ↦ t⁻¹ • D_[f](x + t • w, x, g)) (𝓝[>] 0) (𝓝 0) := by
+  have h := (hderiv.hasLineDerivAt w).tendsto_slope_zero_right.sub_const (g w)
+  rw [sub_self] at h
+  refine h.congr' ?_
+  filter_upwards [self_mem_nhdsWithin] with t ht0
+  simp [bregDiv, smul_sub, ht0.out.ne']
+
+variable [PartialOrder F] [IsOrderedAddMonoid F] [PosSMulMono ℝ F]
+
+/-- Scaled Bregman divergence monotonicity along segments for convex functions. -/
+lemma ConvexOn.bregDiv_slope_le (hf : ConvexOn ℝ s f)
+    {z : E} (hx : x ∈ s) (hz : z ∈ s) (J : E →L[ℝ] F)
+    {t : ℝ} (ht0 : 0 < t) (ht1 : t ≤ 1) :
+    t⁻¹ • D_[f](x + t • (z - x), x, J) ≤ D_[f](z, x, J) := by
+  have : (1 - t) • x + t • z = x + t • (z - x) := by module
+  simpa [this, smul_smul, inv_mul_cancel₀ ht0.ne'] using
+    smul_le_smul_of_nonneg_left
+      ((hf.bregDiv (y := x) J).2 hx hz (sub_nonneg.mpr ht1) ht0.le (sub_add_cancel 1 t))
+      (inv_nonneg.mpr ht0.le)
+
+variable [OrderClosedTopology F]
+
+/-- A Fréchet derivative within `s` of a function convex on `s` is a subgradient on `s`. -/
+lemma HasFDerivWithinAt.hasSubgradientWithinAt
+    (hderiv : HasFDerivWithinAt f g s x) (hf : ConvexOn ℝ s f) (hx : x ∈ s) :
+    HasSubgradientWithinAt f g s x := by
+  intro z hz
+  have h_sub : Set.Ioc (0 : ℝ) 1 ⊆ (fun t : ℝ ↦ x + t • (z - x)) ⁻¹' s \ {0} :=
+    fun t ht ↦ ⟨hf.1.add_smul_sub_mem hx hz ⟨ht.1.le, ht.2⟩, ht.1.ne'⟩
+  have h_le : 𝓝[>] (0 : ℝ) ≤ 𝓝[(fun t : ℝ ↦ x + t • (z - x)) ⁻¹' s \ {0}] 0 := by
+    rw [← nhdsWithin_Ioc_eq_nhdsGT zero_lt_one]
+    exact nhdsWithin_mono _ h_sub
+  refine le_of_tendsto ((hderiv.tendsto_bregDiv_slope_zero (z - x)).mono_left h_le) ?_
+  filter_upwards [self_mem_nhdsWithin, nhdsWithin_le_nhds (eventually_le_nhds zero_lt_one)]
+    with t (ht0 : 0 < t) ht1 using hf.bregDiv_slope_le hx hz g ht0 ht1
+
+/-- A Fréchet derivative of a convex function is a subgradient. -/
+lemma HasFDerivAt.hasSubgradientWithinAt
+    (hderiv : HasFDerivAt f g x) (hf : ConvexOn ℝ s f) (hx : x ∈ s) :
+    HasSubgradientWithinAt f g s x :=
+  hderiv.hasFDerivWithinAt.hasSubgradientWithinAt hf hx
+
+lemma HasFDerivAt.le_of_hasSubgradientWithinAt
+    (hderiv : HasFDerivAt f g x) (hs : s ∈ 𝓝 x) (hsub : HasSubgradientWithinAt f h s x) (w : E) :
+    h w ≤ g w := by
+  have h_nhds : (fun t : ℝ ↦ x + t • w) ⁻¹' s ∈ 𝓝 0 :=
+    (continuous_const.add (continuous_id'.smul continuous_const)).continuousAt.preimage_mem_nhds
+      (by simpa using hs)
+  refine ge_of_tendsto (hderiv.hasLineDerivAt w).tendsto_slope_zero_right ?_
+  filter_upwards [nhdsWithin_le_nhds h_nhds, self_mem_nhdsWithin] with t ht_s (ht_pos : 0 < t)
+  have h_le := smul_le_smul_of_nonneg_left (sub_nonneg.mp (hsub (x + t • w) ht_s))
+    (inv_nonneg.mpr ht_pos.le)
+  simp only [add_sub_cancel_left, map_smul] at h_le
+  rwa [← smul_assoc, smul_eq_mul, inv_mul_cancel₀ (by positivity), one_smul] at h_le
+
+/-- Uniqueness of the subgradient at an interior differentiable point. -/
+lemma HasFDerivAt.eq_of_hasSubgradientWithinAt
+    (hderiv : HasFDerivAt f g x) (hs : s ∈ 𝓝 x) (hsub : HasSubgradientWithinAt f h s x) :
+    h = g := by
+  ext v
+  exact le_antisymm (hderiv.le_of_hasSubgradientWithinAt hs hsub v)
+    (by simpa using hderiv.le_of_hasSubgradientWithinAt hs hsub (-v))
+
+/-- The subdifferential of a convex, differentiable function at an interior point
+is the singleton containing its derivative. -/
+lemma HasFDerivAt.subdifferentialWithin_eq
+    (hderiv : HasFDerivAt f g x) (hf : ConvexOn ℝ s f) (hs : s ∈ 𝓝 x) :
+    ∂[ℝ, s, x](f) = {g} := by
+  ext h
+  simp only [mem_subdifferentialWithin, Set.mem_singleton_iff]
+  exact ⟨fun hsub ↦ hderiv.eq_of_hasSubgradientWithinAt hs hsub,
+    fun h_eq ↦ h_eq ▸ hderiv.hasSubgradientWithinAt hf (mem_of_mem_nhds hs)⟩
+
+/-- The subdifferential of a constant function at an interior point is `{0}`
+(the normal cone to `s` at an interior point is trivial). -/
+lemma subdifferentialWithin_const_eq (c : F) (hs : s ∈ 𝓝 x) :
+    ∂[ℝ, s, x](fun _ : E ↦ c) = {(0 : E →L[ℝ] F)} := by
+  ext h
+  simp only [mem_subdifferentialWithin, Set.mem_singleton_iff]
+  exact ⟨fun hsub ↦ (hasFDerivAt_const c x).eq_of_hasSubgradientWithinAt hs hsub,
+    fun h_eq ↦ h_eq ▸ hasSubgradientWithinAt_const c⟩
+
+/-- Subdifferential sum rule when `f₁` is convex and Fréchet differentiable at `x`
+and `f₂` is convex on `s`: `g` is a subgradient of `f₁ + f₂` at `x` if and only if
+`g - g₁` is a subgradient of `f₂` at `x`. -/
+lemma HasFDerivAt.hasSubgradientWithinAt_add_iff {f₁ f₂ : E → F} {g₁ g : E →L[ℝ] F}
+    (hderiv₁ : HasFDerivAt f₁ g₁ x) (hf₁ : ConvexOn ℝ s f₁) (hf₂ : ConvexOn ℝ s f₂) (hx : x ∈ s) :
+    HasSubgradientWithinAt (f₁ + f₂) g s x ↔ HasSubgradientWithinAt f₂ (g - g₁) s x := by
+  constructor
+  · intro hg z hz
+    refine le_of_tendsto (by simpa using (hderiv₁.tendsto_bregDiv_slope_zero (z - x)).neg) ?_
+    filter_upwards [self_mem_nhdsWithin, nhdsWithin_le_nhds (eventually_le_nhds zero_lt_one)]
+      with t (ht0 : 0 < t) ht1
+    have h_nonneg := smul_nonneg (inv_nonneg.mpr ht0.le)
+      (hg _ (hf₂.1.add_smul_sub_mem hx hz ⟨ht0.le, ht1⟩))
+    rw [(add_sub_cancel g₁ g).symm, bregDiv_add, smul_add, ← neg_le_iff_add_nonneg'] at h_nonneg
+    exact h_nonneg.trans (hf₂.bregDiv_slope_le hx hz (g - g₁) ht0 ht1)
+  · intro h₂
+    simpa using (hderiv₁.hasSubgradientWithinAt hf₁ hx).add h₂
+
+/-- Subdifferential sum rule in set form: `∂[ℝ, s, x](f₁ + f₂) = {g₁} + ∂[ℝ, s, x](f₂)`. -/
+lemma HasFDerivAt.subdifferentialWithin_add {f₁ f₂ : E → F} {g₁ : E →L[ℝ] F}
+    (hderiv₁ : HasFDerivAt f₁ g₁ x) (hf₁ : ConvexOn ℝ s f₁) (hf₂ : ConvexOn ℝ s f₂) (hx : x ∈ s) :
+    ∂[ℝ, s, x](f₁ + f₂) = {g₁} + ∂[ℝ, s, x](f₂) := by
+  ext g
+  simp [mem_subdifferentialWithin, Set.singleton_add,
+    hderiv₁.hasSubgradientWithinAt_add_iff hf₁ hf₂ hx, add_comm g₁, sub_eq_add_neg]
+
+/-- When `f` is convex and Fréchet differentiable at `x ∈ s`, its subdifferential
+is `g + ∂[ℝ, s, x](0)` (the derivative plus the normal cone to `s` at `x`). -/
+lemma HasFDerivAt.subdifferentialWithin_eq_add_zero
+    (hderiv : HasFDerivAt f g x) (hf : ConvexOn ℝ s f) (hx : x ∈ s) :
+    ∂[ℝ, s, x](f) = {g} + ∂[ℝ, s, x](fun _ : E ↦ (0 : F)) := by
+  rw [← add_zero f]
+  exact hderiv.subdifferentialWithin_add hf (convexOn_const (0 : F) hf.1) hx