Adds Fenchel conjugates

LeanMachineLearning.lean

@@ -1,5 +1,10 @@
 module  -- shake: keep-all --deprecated_module: ignore
 
+public import LeanMachineLearning.ForMathlib.Analysis.Convex.Bregman.Basic
+public import LeanMachineLearning.ForMathlib.Analysis.Convex.FenchelConjugate.Basic
+public import LeanMachineLearning.ForMathlib.Analysis.Convex.FenchelConjugate.Calculus
+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

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

LeanMachineLearning/ForMathlib/Analysis/Convex/FenchelConjugate/Basic.lean

@@ -0,0 +1,133 @@
+/-
+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.Algebra.Order.Group.CompleteLattice
+public import Mathlib.Analysis.Normed.Operator.Bilinear
+public import Mathlib.Order.ConditionallyCompleteLattice.Basic
+
+/-!
+# Fenchel Conjugates (Legendre–Fenchel Transform)
+
+This file defines the domain-constrained generalized Fenchel conjugate `f^*[s]`
+for functions `f : E → F` into conditionally complete ordered groups `F`.
+
+It establishes Fenchel–Young inequalities, the equivalence between subgradient
+membership and Fenchel–Young equality, and dual Bregman divergence identities.
+
+## Main definitions
+
+* `fenchelConjugateWithin f s`: The Fenchel conjugate
+  $f^*[s](g) = \sup_{x \in s} (g(x) - f(x))$.
+* `rangeSubdifferentialWithin f s`: The range of the subdifferential operator
+  $\bigcup_{y \in s} \partial[s, y] f$.
+
+## Notation
+
+* `f^*[s]`: Scoped notation in `Bregman` for `fenchelConjugateWithin f s`.
+
+## Main results
+
+* `fenchel_young`: Fenchel–Young inequality $g(x) \le f(x) + f^*[s](g)$.
+* `fenchel_young_eq`: Equivalence
+  $f(x) + f^*[s](g) = g(x) \iff g \in \partial[s, x] f$.
+* `bregman_eq_dual_bregman`: Bregman duality
+  $D_f(x, y, g_y) = D_{f^*[s]}(g_y, g_x, x)$.
+* `dual_subgradient`: Dual subgradient identity
+  $x \in \partial[\text{rangeSubdifferentialWithin } f s, g_x] f^*[s]$.
+-/
+
+@[expose] public section
+
+variable {R E F : Type*} [Ring R]
+  [AddCommGroup E] [Module R E] [TopologicalSpace E]
+  [AddCommGroup F] [Module R F] [TopologicalSpace F] [IsTopologicalAddGroup F]
+  [ConditionallyCompleteLattice F] [IsOrderedAddMonoid F]
+
+/-! ### 1. Definitions and Notation -/
+
+/-- The Fenchel conjugate of `f : E → F` evaluated at `g : E →L[R] F` over a set `s`.
+Defined as $f^*[s](g) = \sup_{x \in s} (g(x) - f(x))$. -/
+noncomputable def fenchelConjugateWithin (f : E → F) (s : Set E) (g : E →L[R] F) : F :=
+  ⨆ x : s, (g x.1 - f x.1)
+
+/-- Scoped notation for Fenchel conjugate on a set `s`. -/
+scoped[Bregman] notation:max f "^*[" s "]" => fenchelConjugateWithin f s
+
+open scoped Bregman
+
+variable {s : Set E} {f : E → F} {x y : E} {g gx gy : E →L[R] F}
+
+omit [ConditionallyCompleteLattice F] [IsOrderedAddMonoid F] in
+lemma fenchel_objective_eq_bregman (f : E → F) (x y : E) (g gy : E →L[R] F) :
+    g x - f x = (g y - f y) + (g - gy) (x - y) - D_[f](x, y, gy) := by
+  simp only [bregDiv, sub_apply, map_sub]
+  abel
+
+/-! ### 2. Fenchel–Young Inequality and Subgradients -/
+
+omit [IsTopologicalAddGroup F] in
+/-- Fenchel–Young inequality: $g(x) \le f(x) + f^*[s](g)$ for all $x \in s$. -/
+lemma fenchel_young (hx : x ∈ s)
+    (hbd : BddAbove (Set.range (fun (y : s) ↦ g y.1 - f y.1))) :
+    g x ≤ f x + f^*[s] g :=
+  sub_le_iff_le_add'.mp (le_ciSup hbd ⟨x, hx⟩)
+
+/-- Characterization of subgradients via Fenchel–Young equality. -/
+lemma fenchel_young_eq (hx : x ∈ s) :
+    (f x + f^*[s] g = g x ∧ BddAbove (Set.range (fun (y : s) ↦ g y.1 - f y.1))) ↔
+      HasSubgradientWithinAt f g s x := by
+  have : Nonempty s := ⟨⟨x, hx⟩⟩
+  constructor
+  · rintro ⟨h, hbd⟩ y hy
+    have h_le : g y - f y ≤ f^*[s] g := le_ciSup hbd ⟨y, hy⟩
+    simp_all [fenchel_objective_eq_bregman f y x g g, eq_sub_of_add_eq' h]
+  · intro h
+    have h_le (y : s) : g y.1 - f y.1 ≤ g x - f x := by
+      simpa [fenchel_objective_eq_bregman f y.1 x g g] using sub_le_self (g x - f x) (h y.1 y.2)
+    have hbd : BddAbove (Set.range (fun (y : s) ↦ g y.1 - f y.1)) :=
+      ⟨_, by rintro _ ⟨y, rfl⟩; exact h_le y⟩
+    have h_eq : f^*[s] g = g x - f x := le_antisymm (ciSup_le h_le) (le_ciSup hbd ⟨x, hx⟩)
+    exact ⟨by simp [h_eq], hbd⟩
+
+/-- The Fenchel conjugate at any subgradient is exactly $g(x) - f(x)$. -/
+lemma HasSubgradientWithinAt.fenchelConjugateWithin (h : HasSubgradientWithinAt f g s x)
+    (hx : x ∈ s) :
+    f^*[s] g = g x - f x :=
+  eq_sub_of_add_eq' ((fenchel_young_eq hx).2 h).1
+
+/-! ### 3. Dual Space and Dual Subgradients -/
+
+/-- The range of the subdifferential operator over `s`,
+defined as $\bigcup_{y \in s} \partial[s, y] f$. -/
+def rangeSubdifferentialWithin (f : E → F) (s : Set E) : Set (E →L[R] F) :=
+  { g | ∃ y ∈ s, HasSubgradientWithinAt f g s y }
+
+section NormedDual
+
+variable {R E F : Type*} [NontriviallyNormedField R]
+  [NormedAddCommGroup E] [NormedSpace R E]
+  [NormedAddCommGroup F] [NormedSpace R F]
+  [ConditionallyCompleteLattice F] [IsOrderedAddMonoid F]
+
+lemma bregman_eq_dual_bregman {s : Set E} {f : E → F}
+    {x y : E} {gx gy : E →L[R] F}
+    (hx : x ∈ s) (h_gx : HasSubgradientWithinAt f gx s x)
+    (hy : y ∈ s) (h_gy : HasSubgradientWithinAt f gy s y) :
+    D_[f](x, y, gy) = D_[f^*[s]](gy, gx, ContinuousLinearMap.apply R F x) := by
+  dsimp [bregDiv]
+  simp only [h_gx.fenchelConjugateWithin hx, h_gy.fenchelConjugateWithin hy, map_sub, sub_apply]
+  abel
+
+lemma dual_subgradient {s : Set E} {f : E → F}
+    {x : E} {gx : E →L[R] F}
+    (hx : x ∈ s) (h_gx : HasSubgradientWithinAt f gx s x) :
+    HasSubgradientWithinAt (f^*[s]) (ContinuousLinearMap.apply R F x)
+      (rangeSubdifferentialWithin f s) gx :=
+  fun _ ⟨_, hy, h_gy⟩ ↦ (bregman_eq_dual_bregman hx h_gx hy h_gy) ▸ h_gy x hx
+
+end NormedDual