From e746e1e7576dc8e19b5c3357f6f6f5abf9f881ca Mon Sep 17 00:00:00 2001 From: ISIPINK Date: Tue, 15 Sep 2026 10:07:29 +0200 Subject: [PATCH 01/15] defined Bregman and properties --- .../ForMathlib/ConvexAnalysis/Bregman.lean | 204 ++++++++++++++++++ 1 file changed, 204 insertions(+) create mode 100644 LeanMachineLearning/ForMathlib/ConvexAnalysis/Bregman.lean diff --git a/LeanMachineLearning/ForMathlib/ConvexAnalysis/Bregman.lean b/LeanMachineLearning/ForMathlib/ConvexAnalysis/Bregman.lean new file mode 100644 index 00000000..76632849 --- /dev/null +++ b/LeanMachineLearning/ForMathlib/ConvexAnalysis/Bregman.lean @@ -0,0 +1,204 @@ +/- +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.Tactic + +/-! +# 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 + +* `Analysis.Convex.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 + an additive map `J : E →+ 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 + +namespace Analysis.Convex + +variable {E F G : Type*} [AddCommGroup E] [AddCommGroup F] [AddCommGroup G] + +/-- The generalized vector-valued Bregman divergence. +`f` maps `E → F`. `J` is the Jacobian / subgradient additive mapping `E →+ F`. -/ +def bregDiv (f : E → F) (x y : E) (J : E →+ F) : F := + f x - f y - J (x - y) + +scoped[Bregman] notation "D_[" f "](" x ", " y ", " J ")" => Analysis.Convex.bregDiv f x y J + +open scoped Bregman + +@[app_unexpander bregDiv] +meta def unexpandBregDiv : Lean.PrettyPrinter.Unexpander + | `($_ $f $x $y $J) => `(D_[$f]($x, $y, $J)) + | _ => throw () + +@[simp] +lemma bregDiv_self (f : E → F) (x : E) (J_x : E →+ F) : + D_[f](x, x, J_x) = 0 := by + simp [bregDiv] + +lemma bregDiv_three_point (f : E → F) (x y z : E) (J_x J_y : E →+ 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, AddMonoidHom.sub_apply] + abel + +lemma bregDiv_add_swap (f : E → F) (x y : E) (J_x J_y : E →+ 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, AddMonoidHom.sub_apply] + abel + +lemma bregDiv_fun_bregDiv (f : E → F) (x y z : E) (J_x J_y : E →+ 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, AddMonoidHom.sub_apply] + abel + +lemma bregDiv_add (f₁ f₂ : E → F) (x y : E) (J₁ J₂ : 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, AddMonoidHom.add_apply, map_sub] + abel + +lemma bregDiv_prod {E₁ E₂ : Type*} [AddCommGroup E₁] [AddCommGroup E₂] + (f₁ : E₁ → F) (f₂ : E₂ → F) (x y : E₁ × E₂) (J₁ : E₁ →+ F) (J₂ : E₂ →+ 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, AddMonoidHom.coprod_apply, map_sub] + abel + +@[simp] +lemma bregDiv_const (c : F) (x y : E) : + D_[fun _ ↦ c](x, y, 0) = 0 := by + simp [bregDiv] + +@[simp] +lemma bregDiv_linear (h : E →+ F) (x y : E) : + D_[h](x, y, h) = 0 := by + simp [bregDiv] + +@[simp] +lemma bregDiv_add_const (f : E → F) (c : F) (x y : E) (J : E →+ 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) (f : E → F) (x y : E) (J : E →+ F) : + D_[fun z ↦ c + f z](x, y, J) = D_[f](x, y, J) := by + simp [bregDiv] + +@[simp] +lemma bregDiv_add_linear (f : E → F) (h : E →+ F) (x y : E) (J : E →+ F) : + D_[fun z ↦ f z + h z](x, y, J + h) = D_[f](x, y, J) := by + simp only [bregDiv, AddMonoidHom.add_apply, map_sub] + abel + +@[simp] +lemma bregDiv_neg (f : E → F) (x y : E) (J : E →+ F) : + D_[-f](x, y, -J) = - D_[f](x, y, J) := by + simp only [bregDiv, Pi.neg_apply, AddMonoidHom.neg_apply, map_sub] + abel + +lemma bregDiv_comp_neg (f : E → F) (x y : E) (J : E →+ F) : + D_[fun z ↦ f (-z)](x, y, -J) = D_[f](-x, -y, J) := by + simp [bregDiv, map_sub] + +lemma bregDiv_translate (f : E → F) (x₀ : E) (x y : E) (J : E →+ F) : + D_[fun z ↦ f (z + x₀)](x, y, J) = D_[f](x + x₀, y + x₀, J) := by + simp [bregDiv] + +section ChainRules + +lemma bregDiv_comp_affine {E₁ : Type*} [AddCommGroup E₁] + (f : E → F) (A : E₁ →+ E) (b : E) (x y : E₁) (J : E →+ F) : + 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 (f₂ : F → G) (f₁ : E → F) (x y : E) (J₂ : F →+ G) (J₁ : E →+ F) : + 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] + +/-- First-order product rule for Bregman divergences. -/ +lemma bregDiv_mul (f₁ f₂ : E → R) (x y : E) (J₁ J₂ : E →+ 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, AddMonoidHom.add_apply, AddMonoidHom.smul_apply, map_sub, smul_eq_mul] + ring + + +end CommRing + +section Order + +variable {F' : Type*} [AddCommGroup F'] [Preorder F'] [AddRightMono F'] + +lemma bregDiv_le_of_le_of_eq {f₁ f₂ : E → F'} {x y : E} {J_y : E →+ 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 F] + +lemma bregDiv_smul (c : R) (f : E → F) (x y : E) (J : E →+ F) : + D_[c • f](x, y, c • J) = c • D_[f](x, y, J) := by + simp [bregDiv, smul_sub] + +lemma bregDiv_convexCombination (f : E → F) (x y : E) (J₁ J₂ : E →+ F) (w : R) : + D_[f](x, y, w • J₁ + (1 - w) • J₂) = w • D_[f](x, y, J₁) + (1 - w) • D_[f](x, y, J₂) := by + calc + D_[f](x, y, w • J₁ + (1 - w) • J₂) + = D_[(w + (1 - w)) • f](x, y, w • J₁ + (1 - w) • J₂) := by + rw [add_sub_cancel, one_smul] + _ = D_[w • f](x, y, w • J₁) + D_[(1 - w) • f](x, y, (1 - w) • J₂) := by + rw [add_smul, bregDiv_add] + _ = w • D_[f](x, y, J₁) + (1 - w) • D_[f](x, y, J₂) := by + simp only [bregDiv_smul] + +end Module + +section Convexity + +variable {𝕜 E' F' : Type*} [Semiring 𝕜] [PartialOrder 𝕜] +variable [AddCommGroup E'] [Module 𝕜 E'] +variable [AddCommGroup F'] [Module 𝕜 F'] [PartialOrder F'] [IsOrderedAddMonoid F'] + +/-- If `f` is convex on `s`, then `x ↦ D_[f](x, y, J)` is convex on `s` for any linear map `J`. -/ +lemma _root_.ConvexOn.bregDiv {s : Set E'} {f : E' → F'} (hf : ConvexOn 𝕜 s f) + (J : E' →ₗ[𝕜] F') (y : E') : + ConvexOn 𝕜 s (fun x ↦ D_[f](x, y, J)) := by + simp only [Analysis.Convex.bregDiv, sub_eq_add_neg, map_add, map_neg, neg_add_rev, neg_neg] + apply ConvexOn.add + · apply ConvexOn.add + · exact hf + · exact convexOn_const (-f y) hf.1 + · apply ConvexOn.add + · exact convexOn_const (J y) hf.1 + · exact (-J).convexOn hf.1 + +end Convexity + +end Analysis.Convex From 1784129afccd28cc6abe6e302d4e14bbdc97cd4d Mon Sep 17 00:00:00 2001 From: ISIPINK Date: Tue, 15 Sep 2026 12:14:39 +0200 Subject: [PATCH 02/15] Import Bregman in LeanMachineLearning.lean --- LeanMachineLearning.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/LeanMachineLearning.lean b/LeanMachineLearning.lean index 3d683931..238d49e2 100644 --- a/LeanMachineLearning.lean +++ b/LeanMachineLearning.lean @@ -1,5 +1,6 @@ module -- shake: keep-all --deprecated_module: ignore +public import LeanMachineLearning.ForMathlib.ConvexAnalysis.Bregman public import LeanMachineLearning.ForMathlib.InformationTheory.KullbackLeibler.ChainRule public import LeanMachineLearning.ForMathlib.InformationTheory.KullbackLeibler.CompProd public import LeanMachineLearning.ForMathlib.InformationTheory.KullbackLeibler.Convex From 55fa914a97ed5d3fbb08d7308236f52a54b43dd3 Mon Sep 17 00:00:00 2001 From: ISIPINK Date: Tue, 15 Sep 2026 12:48:28 +0200 Subject: [PATCH 03/15] Restructure Bregman module into folder with Basic.lean --- LeanMachineLearning.lean | 2 +- .../ConvexAnalysis/{Bregman.lean => Bregman/Basic.lean} | 2 ++ 2 files changed, 3 insertions(+), 1 deletion(-) rename LeanMachineLearning/ForMathlib/ConvexAnalysis/{Bregman.lean => Bregman/Basic.lean} (99%) diff --git a/LeanMachineLearning.lean b/LeanMachineLearning.lean index 238d49e2..52d467d4 100644 --- a/LeanMachineLearning.lean +++ b/LeanMachineLearning.lean @@ -1,6 +1,6 @@ module -- shake: keep-all --deprecated_module: ignore -public import LeanMachineLearning.ForMathlib.ConvexAnalysis.Bregman +public import LeanMachineLearning.ForMathlib.ConvexAnalysis.Bregman.Basic 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/ConvexAnalysis/Bregman.lean b/LeanMachineLearning/ForMathlib/ConvexAnalysis/Bregman/Basic.lean similarity index 99% rename from LeanMachineLearning/ForMathlib/ConvexAnalysis/Bregman.lean rename to LeanMachineLearning/ForMathlib/ConvexAnalysis/Bregman/Basic.lean index 76632849..d34f4e32 100644 --- a/LeanMachineLearning/ForMathlib/ConvexAnalysis/Bregman.lean +++ b/LeanMachineLearning/ForMathlib/ConvexAnalysis/Bregman/Basic.lean @@ -38,10 +38,12 @@ variable {E F G : Type*} [AddCommGroup E] [AddCommGroup F] [AddCommGroup G] def bregDiv (f : E → F) (x y : E) (J : E →+ F) : F := f x - f y - J (x - y) +/-- Scoped notation for `bregDiv`. -/ scoped[Bregman] notation "D_[" f "](" x ", " y ", " J ")" => Analysis.Convex.bregDiv f x y J open scoped Bregman +/-- Unexpander for `bregDiv`. -/ @[app_unexpander bregDiv] meta def unexpandBregDiv : Lean.PrettyPrinter.Unexpander | `($_ $f $x $y $J) => `(D_[$f]($x, $y, $J)) From a20977e81778d87077d49200069ab2124377473c Mon Sep 17 00:00:00 2001 From: ISIPINK Date: Tue, 15 Sep 2026 12:14:14 +0200 Subject: [PATCH 04/15] added subgrad def & props --- LeanMachineLearning.lean | 1 + .../ConvexAnalysis/Subgradient.lean | 216 ++++++++++++++++++ 2 files changed, 217 insertions(+) create mode 100644 LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient.lean diff --git a/LeanMachineLearning.lean b/LeanMachineLearning.lean index 52d467d4..f67807c3 100644 --- a/LeanMachineLearning.lean +++ b/LeanMachineLearning.lean @@ -1,6 +1,7 @@ module -- shake: keep-all --deprecated_module: ignore public import LeanMachineLearning.ForMathlib.ConvexAnalysis.Bregman.Basic +public import LeanMachineLearning.ForMathlib.ConvexAnalysis.Subgradient 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/ConvexAnalysis/Subgradient.lean b/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient.lean new file mode 100644 index 00000000..22a69fb6 --- /dev/null +++ b/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient.lean @@ -0,0 +1,216 @@ +/- +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.ConvexAnalysis.Bregman.Basic +public import Mathlib.Analysis.Convex.Function +public import Mathlib.Order.ConditionallyCompleteLattice.Basic +public import Mathlib.Tactic + +/-! +# Subgradients and Subdifferentials + +Subgradients of functions `f : E → F` defined +via the non-negativity of the Bregman divergence `0 ≤ D_[f](x, y, g_y)` on an explicit +domain `V` (i.e. the linearization error is non-negative on `V`). + +Carrying the domain `V : Set E` explicitly avoids using indicator functions +while supporting constrained convex analysis. + +## Main definitions + +* `Analysis.Convex.IsSubgradient V f y g_y`: `g_y : E →+ F` is a subgradient of `f` at `y` on `V`. +* `Analysis.Convex.subdifferential V f y`: The subdifferential set `∂[V, y] f`. + +## Main results + +* Chain rules: `Analysis.Convex.IsSubgradient.comp_affine` and `Analysis.Convex.IsSubgradient.comp`. +* Equivalence with classical inequality: `Analysis.Convex.mem_subdifferential_iff_le`. +* Fermat's rule: `Analysis.Convex.zero_mem_subdifferential_iff_isMinOn`. +* Suprema and maxima: `Analysis.Convex.IsSubgradient.max_left`, + `Analysis.Convex.IsSubgradient.max_right`, `Analysis.Convex.IsSubgradient.finset_sup`, + and `Analysis.Convex.IsSubgradient.ciSup`. + +## Notation + +* `∂[V, y] f`: Scoped notation in `Bregman` for `subdifferential V f y`. +-/ + +@[expose] public section + +namespace Analysis.Convex + +open scoped Bregman + +variable {E F : Type*} [AddCommGroup E] [AddCommGroup F] [Preorder F] + +/-- `g_y` is a subgradient of `f` at `y` on domain `V` (non-negativity of Bregman divergence). -/ +def IsSubgradient (V : Set E) (f : E → F) (y : E) (g_y : E →+ F) : Prop := + y ∈ V ∧ ∀ x ∈ V, 0 ≤ D_[f](x, y, g_y) + +/-- The subdifferential `∂[V, y] f` of `f` at `y` on `V`. -/ +def subdifferential (V : Set E) (f : E → F) (y : E) : Set (E →+ F) := + { g | IsSubgradient V f y g } + +scoped[Bregman] notation:60 "∂[" V ", " y "] " f:50 => Analysis.Convex.subdifferential V f y + +@[app_unexpander subdifferential] +meta def unexpandSubdifferential : Lean.PrettyPrinter.Unexpander + | `($_ $V $f $y) => `(∂[$V, $y] $f) + | _ => throw () + +variable {V : Set E} {f : E → F} {y x : E} {g_y : E →+ F} + +@[local simp] +lemma mem_subdifferential_iff : + g_y ∈ ∂[V, y] f ↔ y ∈ V ∧ ∀ x ∈ V, 0 ≤ D_[f](x, y, g_y) := Iff.rfl + +@[simp] +lemma mem_subdifferential_const_iff {c : F} : + (0 : E →+ F) ∈ ∂[V, y] (fun _ ↦ c) ↔ y ∈ V := by simp + +@[simp] +lemma mem_subdifferential_linear_iff {h : E →+ F} : + h ∈ ∂[V, y] h ↔ y ∈ V := by simp + +@[simp] +lemma mem_subdifferential_add_const_iff {c : F} : + g_y ∈ ∂[V, y] (fun x ↦ f x + c) ↔ g_y ∈ ∂[V, y] f := by simp + +@[simp] +lemma mem_subdifferential_const_add_iff {c : F} : + g_y ∈ ∂[V, y] (fun x ↦ c + f x) ↔ g_y ∈ ∂[V, y] f := by simp + +@[simp] +lemma mem_subdifferential_add_linear_iff {h : E →+ F} : + (g_y + h) ∈ ∂[V, y] (fun x ↦ f x + h x) ↔ g_y ∈ ∂[V, y] f := by simp + +@[simp] +lemma mem_subdifferential_bregDiv_iff {g_x g_y : E →+ F} : + (g_x - g_y) ∈ ∂[V, x] (fun z ↦ D_[f](z, y, g_y)) ↔ g_x ∈ ∂[V, x] f := by + simp [bregDiv_fun_bregDiv] + +lemma zero_mem_subdifferential_iff : + (0 : E →+ F) ∈ ∂[V, y] f ↔ y ∈ V ∧ ∀ x ∈ V, 0 ≤ f x - f y := by simp [bregDiv] + +lemma IsSubgradient.comp_affine {E₁ : Type*} [AddCommGroup E₁] + {V₁ : Set E₁} {y₁ : E₁} {A : E₁ →+ E} {b : E} + (hy₁ : y₁ ∈ V₁) (h_map : ∀ x ∈ V₁, A x + b ∈ V) + (h_sub : g_y ∈ ∂[V, A y₁ + b] f) : + (g_y.comp A) ∈ ∂[V₁, y₁] (fun x ↦ f (A x + b)) := + ⟨hy₁, fun x hx ↦ by simp [bregDiv_comp_affine, h_sub.2 (A x + b) (h_map x hx)]⟩ + +/-- **Chain rule**: `g₂ ∘ g₁` is a subgradient of `f₂ ∘ f₁` when `g₂` is non-negative. -/ +lemma IsSubgradient.comp {G : Type*} [AddCommGroup G] [Preorder G] [IsOrderedAddMonoid G] + {f₂ : F → G} {f₁ : E → F} {g₂ : F →+ G} {g₁ : E →+ F} + (h₂ : g₂ ∈ ∂[f₁ '' V, f₁ y] f₂) (h₁ : g₁ ∈ ∂[V, y] f₁) + (hg₂_nonneg : ∀ z ≥ 0, 0 ≤ g₂ z) : + (g₂.comp g₁) ∈ ∂[V, y] (f₂ ∘ f₁) := + ⟨h₁.1, fun x hx ↦ by + simp only [bregDiv_comp, add_nonneg (h₂.2 (f₁ x) ⟨x, hx, rfl⟩) (hg₂_nonneg _ (h₁.2 x hx))]⟩ + +section OrderedGroup + +variable [IsOrderedAddMonoid F] + +/-- Equivalence with the classical definition. -/ +lemma mem_subdifferential_iff_le : + g_y ∈ ∂[V, y] f ↔ y ∈ V ∧ ∀ x ∈ V, f y + g_y (x - y) ≤ f x := by + simp [bregDiv, sub_sub, sub_nonneg] + +lemma IsSubgradient.monotonicity {g_x : E →+ F} + (hx_sub : g_x ∈ ∂[V, x] f) (hy_sub : g_y ∈ ∂[V, y] f) : + 0 ≤ (g_x - g_y) (x - y) := by + rw [← bregDiv_add_swap f x y g_x g_y] + exact add_nonneg (hx_sub.2 y hy_sub.1) (hy_sub.2 x hx_sub.1) + + +/-- **Fermat's rule**: `0` is a subgradient of `f` at `y` iff `y` is a minimizer of `f` on `V`. -/ +lemma zero_mem_subdifferential_iff_isMinOn : + (0 : E →+ F) ∈ ∂[V, y] f ↔ y ∈ V ∧ IsMinOn f V y := by + simp [bregDiv, sub_nonneg, isMinOn_iff] + +lemma IsSubgradient.add {f₁ f₂ : E → F} {g₁ g₂ : E →+ F} + (h₁ : g₁ ∈ ∂[V, y] f₁) (h₂ : g₂ ∈ ∂[V, y] f₂) : + (g₁ + g₂) ∈ ∂[V, y] (f₁ + f₂) := + ⟨h₁.1, fun x hx ↦ by simp [bregDiv_add, add_nonneg (h₁.2 x hx) (h₂.2 x hx)]⟩ + +lemma IsSubgradient.add_isMinOn {f₁ f₂ : E → F} {x : E} {g : E →+ F} + (h_min : IsMinOn f₁ V x) (hx_mem : x ∈ V) (h_sub : g ∈ ∂[V, x] f₂) : + g ∈ ∂[V, x] (f₁ + f₂) := by + simpa using IsSubgradient.add (zero_mem_subdifferential_iff_isMinOn.mpr ⟨hx_mem, h_min⟩) h_sub + +lemma IsSubgradient.of_le_of_eq {f₁ f₂ : E → F} {g_y : E →+ F} + (h_sub : g_y ∈ ∂[V, y] f₁) (h_le : ∀ x ∈ V, f₁ x ≤ f₂ x) (h_eq : f₁ y = f₂ y) : + g_y ∈ ∂[V, y] f₂ := + ⟨h_sub.1, fun x hx ↦ le_trans (h_sub.2 x hx) + (bregDiv_le_of_le_of_eq (h_le x hx) h_eq)⟩ + +end OrderedGroup + +section ModuleBasic + +variable {R : Type*} [CommRing R] [PartialOrder R] [Module R F] [PosSMulMono R F] + +lemma IsSubgradient.smul {c : R} (hc : 0 ≤ c) {f : E → F} {g_y : E →+ F} + (h_sub : g_y ∈ ∂[V, y] f) : + (c • g_y) ∈ ∂[V, y] (c • f) := + ⟨h_sub.1, fun x hx ↦ by simp [bregDiv_smul, smul_nonneg hc (h_sub.2 x hx)]⟩ + +end ModuleBasic + +section Module + +variable {R : Type*} [CommRing R] [PartialOrder R] [IsOrderedRing R] + [IsOrderedAddMonoid F] [Module R F] [PosSMulMono R F] + +lemma IsSubgradient.convexCombination {f : E → F} {g₁ g₂ : E →+ F} + (h₁ : g₁ ∈ ∂[V, y] f) (h₂ : g₂ ∈ ∂[V, y] f) {w : R} (hw : w ∈ Set.Icc (0 : R) 1) : + (w • g₁ + (1 - w) • g₂) ∈ ∂[V, y] f := + ⟨h₁.1, fun x hx ↦ by + simp [bregDiv_convexCombination, hw.1, sub_nonneg.mpr hw.2, + h₁.2 x hx, h₂.2 x hx, smul_nonneg, add_nonneg]⟩ + +end Module + +section LinearOrder + +variable {F_lin : Type*} [AddCommGroup F_lin] [LinearOrder F_lin] [IsOrderedAddMonoid F_lin] + +lemma IsSubgradient.max_left {f₁ f₂ : E → F_lin} {g_y : E →+ F_lin} + (h_sub : g_y ∈ ∂[V, y] f₁) (h_active : f₁ y = max (f₁ y) (f₂ y)) : + g_y ∈ ∂[V, y] (fun x ↦ max (f₁ x) (f₂ x)) := + IsSubgradient.of_le_of_eq h_sub (fun x _ ↦ le_max_left (f₁ x) (f₂ x)) h_active + +lemma IsSubgradient.max_right {f₁ f₂ : E → F_lin} {g_y : E →+ F_lin} + (h_sub : g_y ∈ ∂[V, y] f₂) (h_active : f₂ y = max (f₁ y) (f₂ y)) : + g_y ∈ ∂[V, y] (fun x ↦ max (f₁ x) (f₂ x)) := + IsSubgradient.of_le_of_eq h_sub (fun x _ ↦ le_max_right (f₁ x) (f₂ x)) h_active + +lemma IsSubgradient.finset_sup {ι : Type*} {s : Finset ι} + {f_i : ι → E → F_lin} {i : ι} {g_y : E →+ F_lin} + (his : i ∈ s) + (h_sub : g_y ∈ ∂[V, y] (f_i i)) (h_active : f_i i y = s.sup' ⟨i, his⟩ (fun j ↦ f_i j y)) : + g_y ∈ ∂[V, y] (fun x ↦ s.sup' ⟨i, his⟩ (fun j ↦ f_i j x)) := + IsSubgradient.of_le_of_eq h_sub (fun _ _ ↦ Finset.le_sup'_of_le _ his (le_refl _)) h_active + +end LinearOrder + +section Lattice + +variable {F_lat : Type*} [AddCommGroup F_lat] + [ConditionallyCompleteLattice F_lat] [IsOrderedAddMonoid F_lat] + +lemma IsSubgradient.ciSup {ι : Type*} {f_i : ι → E → F_lat} {i : ι} {g_y : E →+ F_lat} + (h_sub : g_y ∈ ∂[V, y] (f_i i)) + (h_active : f_i i y = ⨆ j, f_i j y) + (h_bdd : ∀ x ∈ V, BddAbove (Set.range (fun j ↦ f_i j x))) : + g_y ∈ ∂[V, y] (fun x ↦ ⨆ j, f_i j x) := + IsSubgradient.of_le_of_eq h_sub (fun x hx ↦ le_ciSup (h_bdd x hx) i) h_active + +end Lattice + +end Analysis.Convex From 2d7dc6ae03d500cc0f1c6e68e0c9a700948115ee Mon Sep 17 00:00:00 2001 From: ISIPINK Date: Tue, 15 Sep 2026 12:49:54 +0200 Subject: [PATCH 05/15] Restructure Subgradient module into folder with Basic.lean --- LeanMachineLearning.lean | 2 +- .../ConvexAnalysis/{Subgradient.lean => Subgradient/Basic.lean} | 2 ++ 2 files changed, 3 insertions(+), 1 deletion(-) rename LeanMachineLearning/ForMathlib/ConvexAnalysis/{Subgradient.lean => Subgradient/Basic.lean} (99%) diff --git a/LeanMachineLearning.lean b/LeanMachineLearning.lean index f67807c3..7780f5c6 100644 --- a/LeanMachineLearning.lean +++ b/LeanMachineLearning.lean @@ -1,7 +1,7 @@ module -- shake: keep-all --deprecated_module: ignore public import LeanMachineLearning.ForMathlib.ConvexAnalysis.Bregman.Basic -public import LeanMachineLearning.ForMathlib.ConvexAnalysis.Subgradient +public import LeanMachineLearning.ForMathlib.ConvexAnalysis.Subgradient.Basic 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/ConvexAnalysis/Subgradient.lean b/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Basic.lean similarity index 99% rename from LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient.lean rename to LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Basic.lean index 22a69fb6..c8774fca 100644 --- a/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient.lean +++ b/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Basic.lean @@ -55,8 +55,10 @@ def IsSubgradient (V : Set E) (f : E → F) (y : E) (g_y : E →+ F) : Prop := def subdifferential (V : Set E) (f : E → F) (y : E) : Set (E →+ F) := { g | IsSubgradient V f y g } +/-- Scoped notation for `subdifferential`. -/ scoped[Bregman] notation:60 "∂[" V ", " y "] " f:50 => Analysis.Convex.subdifferential V f y +/-- Unexpander for `subdifferential`. -/ @[app_unexpander subdifferential] meta def unexpandSubdifferential : Lean.PrettyPrinter.Unexpander | `($_ $V $f $y) => `(∂[$V, $y] $f) From 7b7d742b21377ccf80e346578a054273ba4ca248 Mon Sep 17 00:00:00 2001 From: ISIPINK Date: Tue, 15 Sep 2026 16:13:12 +0200 Subject: [PATCH 06/15] added subgradient deriv connection --- LeanMachineLearning.lean | 1 + .../ConvexAnalysis/Subgradient/Deriv.lean | 102 ++++++++++++++++++ 2 files changed, 103 insertions(+) create mode 100644 LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Deriv.lean diff --git a/LeanMachineLearning.lean b/LeanMachineLearning.lean index 7780f5c6..eeaeecb3 100644 --- a/LeanMachineLearning.lean +++ b/LeanMachineLearning.lean @@ -2,6 +2,7 @@ module -- shake: keep-all --deprecated_module: ignore public import LeanMachineLearning.ForMathlib.ConvexAnalysis.Bregman.Basic public import LeanMachineLearning.ForMathlib.ConvexAnalysis.Subgradient.Basic +public import LeanMachineLearning.ForMathlib.ConvexAnalysis.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/ConvexAnalysis/Subgradient/Deriv.lean b/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Deriv.lean new file mode 100644 index 00000000..1d338392 --- /dev/null +++ b/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Deriv.lean @@ -0,0 +1,102 @@ +/- +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.ConvexAnalysis.Subgradient.Basic +public import Mathlib.Analysis.Calculus.LineDeriv.Basic + +/-! +# Fréchet Derivatives and Subgradients + +This file establishes the connection between Fréchet derivatives (`HasFDerivAt`) +and subgradients (`∂[V, x] f`) for convex functions. + +## Main results + +* `Analysis.Convex.subgradient_of_hasFDerivAt`: A Fréchet derivative of a convex function + is a subgradient. +* `Analysis.Convex.le_fderiv_of_mem_subdifferential`: An interior subgradient is bounded + above by the Fréchet derivative. +* `Analysis.Convex.eq_fderiv_of_mem_subdifferential`: Uniqueness of subgradient at interior + differentiable points. +-/ + +@[expose] public section + +namespace Analysis.Convex + +variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] +variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] +variable [PartialOrder F] [IsOrderedAddMonoid F] [PosSMulMono ℝ F] + +open scoped Bregman +open Asymptotics + +local instance : Coe (E →L[ℝ] F) (E →+ F) where + coe g := g.toAddMonoidHom + +local instance : Membership (E →L[ℝ] F) (Set (E →+ F)) where + mem s g := (g : E →+ F) ∈ s + + +omit [PosSMulMono ℝ F] in +/-- For a convex function, the Bregman divergence at an interpolated point `x + t • (z - x)` +is bounded by `t • D_[f](z, x, J)`. -/ +lemma ConvexOn.bregman_segment_le {f : E → F} {V : Set E} (h_conv : ConvexOn ℝ V f) + {x z : E} (hx : x ∈ V) (hz : z ∈ V) (J : E →ₗ[ℝ] F) + {t : ℝ} (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : + D_[f](x + t • (z - x), x, J) ≤ t • D_[f](z, x, J) := by + have h_comb : (1 - t) • x + t • z = x + t • (z - x) := by module + simpa [h_comb] using + (h_conv.bregDiv (y := x) J).2 hx hz (sub_nonneg.mpr ht1) ht0 (sub_add_cancel 1 t) + +variable [OrderClosedTopology F] + +/-- +For a convex function `f : E → F`, if `f` has a Fréchet derivative at `x` represented by the +continuous linear map `g`, then `g` is a subgradient of `f` at `x` over the set `V`. +-/ +lemma subgradient_of_hasFDerivAt {f : E → F} {V : Set E} {x : E} {g : E →L[ℝ] F} + (h_conv : ConvexOn ℝ V f) (hx : x ∈ V) + (h_deriv : HasFDerivAt f g x) : + g ∈ ∂[V, x] f := by + refine ⟨hx, fun z hz ↦ sub_nonneg.mpr <| + le_of_tendsto (h_deriv.hasLineDerivAt (z - x)).tendsto_slope_zero_right ?_⟩ + filter_upwards [self_mem_nhdsWithin, + Filter.mem_inf_of_left (eventually_le_nhds zero_lt_one)] with t (ht0 : 0 < t) ht1 + simpa [bregDiv, smul_smul, inv_mul_cancel₀ ht0.ne'] using + smul_le_smul_of_nonneg_left + (ConvexOn.bregman_segment_le h_conv hx hz 0 ht0.le ht1) (inv_nonneg.mpr ht0.le) + + +/-- +If `f : E → ℝ` has Fréchet derivative `g` at an interior point `x` of `V`, +then any subgradient `h ∈ ∂[V, x] f` satisfies `h w ≤ g w` for all directions `w`. +-/ +lemma le_fderiv_of_mem_subdifferential {f : E → ℝ} {V : Set E} {x : E} {g h : E →L[ℝ] ℝ} + (hV : V ∈ nhds x) (h_deriv : HasFDerivAt f g x) (h_sub : h ∈ ∂[V, x] f) (w : E) : + h w ≤ g w := by + have h_nhds : (fun t : ℝ ↦ x + t • w) ⁻¹' V ∈ nhds 0 := + (continuous_const.add (continuous_id'.smul continuous_const)).continuousAt.preimage_mem_nhds + (by simpa using hV) + refine ge_of_tendsto (h_deriv.hasLineDerivAt w).tendsto_slope_zero_right ?_ + filter_upwards [nhdsWithin_le_nhds h_nhds, self_mem_nhdsWithin] with t ht_V (ht_pos : 0 < t) + simpa [bregDiv, add_sub_cancel_left, h.map_smul, smul_eq_mul, + inv_mul_cancel_left₀ ht_pos.ne'] using + mul_le_mul_of_nonneg_left (sub_nonneg.mp (h_sub.2 (x + t • w) ht_V)) (inv_nonneg.mpr ht_pos.le) + +/-- +If a function `f : E → ℝ` is Fréchet differentiable at an interior point `x` of `V` with derivative +`g`, then any continuous linear subgradient `h ∈ ∂[V, x] f` must be equal to `g`. +-/ +lemma eq_fderiv_of_mem_subdifferential {f : E → ℝ} {V : Set E} {x : E} {g h : E →L[ℝ] ℝ} + (hV : V ∈ nhds x) (h_deriv : HasFDerivAt f g x) (h_sub : h ∈ ∂[V, x] f) : + h = g := by + ext v + exact le_antisymm (le_fderiv_of_mem_subdifferential hV h_deriv h_sub v) + (by simpa using le_fderiv_of_mem_subdifferential hV h_deriv h_sub (-v)) + +end Analysis.Convex From 3acfb68d1c513806c5018f7826c3a075b220f174 Mon Sep 17 00:00:00 2001 From: ISIPINK Date: Wed, 16 Sep 2026 11:47:58 +0200 Subject: [PATCH 07/15] rw deriv proofs added sum rule (deriv + convex) --- .../ConvexAnalysis/Subgradient/Deriv.lean | 143 ++++++++++++------ 1 file changed, 96 insertions(+), 47 deletions(-) diff --git a/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Deriv.lean b/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Deriv.lean index 1d338392..05cec5ab 100644 --- a/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Deriv.lean +++ b/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Deriv.lean @@ -7,6 +7,7 @@ module public import LeanMachineLearning.ForMathlib.ConvexAnalysis.Subgradient.Basic public import Mathlib.Analysis.Calculus.LineDeriv.Basic +public import Mathlib.Data.Set.Basic /-! # Fréchet Derivatives and Subgradients @@ -16,12 +17,14 @@ and subgradients (`∂[V, x] f`) for convex functions. ## Main results -* `Analysis.Convex.subgradient_of_hasFDerivAt`: A Fréchet derivative of a convex function +* `HasFDerivAt.mem_subdifferential`: A Fréchet derivative of a convex function is a subgradient. -* `Analysis.Convex.le_fderiv_of_mem_subdifferential`: An interior subgradient is bounded +* `HasFDerivAt.le_of_mem_subdifferential`: An interior subgradient is bounded above by the Fréchet derivative. -* `Analysis.Convex.eq_fderiv_of_mem_subdifferential`: Uniqueness of subgradient at interior +* `HasFDerivAt.eq_of_mem_subdifferential`: Uniqueness of subgradient at interior differentiable points. +* `mem_subdifferential_add_hasFDerivAt_iff`: Subdifferential sum rule when one + component is Fréchet differentiable. -/ @[expose] public section @@ -31,27 +34,33 @@ namespace Analysis.Convex variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] variable [PartialOrder F] [IsOrderedAddMonoid F] [PosSMulMono ℝ F] - -open scoped Bregman -open Asymptotics - -local instance : Coe (E →L[ℝ] F) (E →+ F) where - coe g := g.toAddMonoidHom - -local instance : Membership (E →L[ℝ] F) (Set (E →+ F)) where - mem s g := (g : E →+ F) ∈ s - - -omit [PosSMulMono ℝ F] in -/-- For a convex function, the Bregman divergence at an interpolated point `x + t • (z - x)` -is bounded by `t • D_[f](z, x, J)`. -/ -lemma ConvexOn.bregman_segment_le {f : E → F} {V : Set E} (h_conv : ConvexOn ℝ V f) - {x z : E} (hx : x ∈ V) (hz : z ∈ V) (J : E →ₗ[ℝ] F) - {t : ℝ} (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : - D_[f](x + t • (z - x), x, J) ≤ t • D_[f](z, x, J) := by - have h_comb : (1 - t) • x + t • z = x + t • (z - x) := by module - simpa [h_comb] using - (h_conv.bregDiv (y := x) J).2 hx hz (sub_nonneg.mpr ht1) ht0 (sub_add_cancel 1 t) +variable {f : E → F} {V : Set E} {x : E} {g h : E →L[ℝ] F} + +open scoped Bregman Topology +open Asymptotics Filter + +/-- Scaled Bregman divergence monotonicity along segments for convex functions. -/ +lemma _root_.ConvexOn.bregDiv_slope_le (hf : ConvexOn ℝ V f) + {z : E} (hx : x ∈ V) (hz : z ∈ V) (J : E →ₗ[ℝ] 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) + +omit [PartialOrder F] [IsOrderedAddMonoid F] [PosSMulMono ℝ F] in +/-- As the step size `t → 0⁺`, the linearization error of a Fréchet differentiable function +scaled by `t⁻¹` converges to `0`. -/ +lemma _root_.HasFDerivAt.tendsto_bregDiv_slope_zero + (hderiv : HasFDerivAt f g x) (w : E) : + Tendsto (fun t : ℝ ↦ t⁻¹ • D_[f](x + t • w, x, (g : E →+ F))) (𝓝[>] 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 [OrderClosedTopology F] @@ -59,44 +68,84 @@ variable [OrderClosedTopology F] For a convex function `f : E → F`, if `f` has a Fréchet derivative at `x` represented by the continuous linear map `g`, then `g` is a subgradient of `f` at `x` over the set `V`. -/ -lemma subgradient_of_hasFDerivAt {f : E → F} {V : Set E} {x : E} {g : E →L[ℝ] F} - (h_conv : ConvexOn ℝ V f) (hx : x ∈ V) - (h_deriv : HasFDerivAt f g x) : - g ∈ ∂[V, x] f := by - refine ⟨hx, fun z hz ↦ sub_nonneg.mpr <| - le_of_tendsto (h_deriv.hasLineDerivAt (z - x)).tendsto_slope_zero_right ?_⟩ - filter_upwards [self_mem_nhdsWithin, - Filter.mem_inf_of_left (eventually_le_nhds zero_lt_one)] with t (ht0 : 0 < t) ht1 - simpa [bregDiv, smul_smul, inv_mul_cancel₀ ht0.ne'] using - smul_le_smul_of_nonneg_left - (ConvexOn.bregman_segment_le h_conv hx hz 0 ht0.le ht1) (inv_nonneg.mpr ht0.le) +lemma _root_.HasFDerivAt.mem_subdifferential + (hderiv : HasFDerivAt f g x) (hf : ConvexOn ℝ V f) (hx : x ∈ V) : + (g : E →+ F) ∈ ∂[V, x] f := by + refine ⟨hx, fun z hz ↦ le_of_tendsto (hderiv.tendsto_bregDiv_slope_zero (z - x)) ?_⟩ + 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.toLinearMap ht0 ht1 +lemma subgradient_of_hasFDerivAt + (hf : ConvexOn ℝ V f) (hx : x ∈ V) (hderiv : HasFDerivAt f g x) : + (g : E →+ F) ∈ ∂[V, x] f := + hderiv.mem_subdifferential hf hx + +section Real + +variable {f : E → ℝ} {g h : E →L[ℝ] ℝ} /-- If `f : E → ℝ` has Fréchet derivative `g` at an interior point `x` of `V`, -then any subgradient `h ∈ ∂[V, x] f` satisfies `h w ≤ g w` for all directions `w`. +then any continuous linear subgradient `h ∈ ∂[V, x] f` satisfies `h w ≤ g w` for all directions `w`. -/ -lemma le_fderiv_of_mem_subdifferential {f : E → ℝ} {V : Set E} {x : E} {g h : E →L[ℝ] ℝ} - (hV : V ∈ nhds x) (h_deriv : HasFDerivAt f g x) (h_sub : h ∈ ∂[V, x] f) (w : E) : +lemma _root_.HasFDerivAt.le_of_mem_subdifferential + (hderiv : HasFDerivAt f g x) (hV : V ∈ 𝓝 x) (hsub : (h : E →+ ℝ) ∈ ∂[V, x] f) (w : E) : h w ≤ g w := by - have h_nhds : (fun t : ℝ ↦ x + t • w) ⁻¹' V ∈ nhds 0 := + have h_nhds : (fun t : ℝ ↦ x + t • w) ⁻¹' V ∈ 𝓝 0 := (continuous_const.add (continuous_id'.smul continuous_const)).continuousAt.preimage_mem_nhds (by simpa using hV) - refine ge_of_tendsto (h_deriv.hasLineDerivAt w).tendsto_slope_zero_right ?_ + refine ge_of_tendsto (hderiv.hasLineDerivAt w).tendsto_slope_zero_right ?_ filter_upwards [nhdsWithin_le_nhds h_nhds, self_mem_nhdsWithin] with t ht_V (ht_pos : 0 < t) simpa [bregDiv, add_sub_cancel_left, h.map_smul, smul_eq_mul, inv_mul_cancel_left₀ ht_pos.ne'] using - mul_le_mul_of_nonneg_left (sub_nonneg.mp (h_sub.2 (x + t • w) ht_V)) (inv_nonneg.mpr ht_pos.le) + mul_le_mul_of_nonneg_left (sub_nonneg.mp (hsub.2 (x + t • w) ht_V)) (inv_nonneg.mpr ht_pos.le) /-- -If a function `f : E → ℝ` is Fréchet differentiable at an interior point `x` of `V` with derivative -`g`, then any continuous linear subgradient `h ∈ ∂[V, x] f` must be equal to `g`. +If `f : E → ℝ` has Fréchet derivative `g` at an interior point `x` of `V`, +then the subgradient is unique and equal to `g`. -/ -lemma eq_fderiv_of_mem_subdifferential {f : E → ℝ} {V : Set E} {x : E} {g h : E →L[ℝ] ℝ} - (hV : V ∈ nhds x) (h_deriv : HasFDerivAt f g x) (h_sub : h ∈ ∂[V, x] f) : +lemma _root_.HasFDerivAt.eq_of_mem_subdifferential + (hderiv : HasFDerivAt f g x) (hV : V ∈ 𝓝 x) (hsub : (h : E →+ ℝ) ∈ ∂[V, x] f) : h = g := by ext v - exact le_antisymm (le_fderiv_of_mem_subdifferential hV h_deriv h_sub v) - (by simpa using le_fderiv_of_mem_subdifferential hV h_deriv h_sub (-v)) + exact le_antisymm (hderiv.le_of_mem_subdifferential hV hsub v) + (by simpa using hderiv.le_of_mem_subdifferential hV hsub (-v)) + +/-- +Subdifferential sum rule when `f₁` is convex and Fréchet differentiable at `x` +and `f₂` is convex on `V`: `g` is a subgradient of `f₁ + f₂` at `x` if and only if +`g - g₁` is a subgradient of `f₂` at `x`. +-/ +lemma _root_.HasFDerivAt.mem_subdifferential_add_iff {f₁ f₂ : E → ℝ} + {g₁ g : E →L[ℝ] ℝ} + (hderiv₁ : HasFDerivAt f₁ g₁ x) (hf₁ : ConvexOn ℝ V f₁) (hf₂ : ConvexOn ℝ V f₂) (hx : x ∈ V) : + (g : E →+ ℝ) ∈ ∂[V, x] (f₁ + f₂) ↔ (g - g₁ : E →+ ℝ) ∈ ∂[V, x] f₂ := by + have h_eq : (g : E →+ ℝ) = (g₁ : E →+ ℝ) + (g - g₁ : E →+ ℝ) := by ext; simp + constructor + · rintro ⟨-, hg⟩ + refine ⟨hx, fun z hz ↦ 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_slope : t⁻¹ • D_[f₂](x + t • (z - x), x, (g - g₁ : E →+ ℝ)) ≤ + D_[f₂](z, x, (g - g₁ : E →+ ℝ)) := + hf₂.bregDiv_slope_le hx hz (g - g₁).toLinearMap ht0 ht1 + have h_nonneg := smul_nonneg (inv_nonneg.mpr ht0.le) + (hg _ (hf₂.1.add_smul_sub_mem hx hz ⟨ht0.le, ht1⟩)) + rw [h_eq, bregDiv_add, smul_add] at h_nonneg + dsimp at * + linarith + · intro h₂ + have := IsSubgradient.add (hderiv₁.mem_subdifferential hf₁ hx) h₂ + rwa [← h_eq] at this + +lemma mem_subdifferential_add_hasFDerivAt_iff {f₁ f₂ : E → ℝ} + {g₁ g : E →L[ℝ] ℝ} + (hf₁ : ConvexOn ℝ V f₁) (hf₂ : ConvexOn ℝ V f₂) (hx : x ∈ V) + (hderiv₁ : HasFDerivAt f₁ g₁ x) : + (g : E →+ ℝ) ∈ ∂[V, x] (f₁ + f₂) ↔ (g - g₁ : E →+ ℝ) ∈ ∂[V, x] f₂ := + hderiv₁.mem_subdifferential_add_iff hf₁ hf₂ hx + +end Real end Analysis.Convex From a4b0f3e64634b27c66875eb35c936b0a6761238c Mon Sep 17 00:00:00 2001 From: ISIPINK Date: Wed, 16 Sep 2026 11:56:30 +0200 Subject: [PATCH 08/15] updated comments --- .../ConvexAnalysis/Subgradient/Deriv.lean | 14 ++------------ 1 file changed, 2 insertions(+), 12 deletions(-) diff --git a/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Deriv.lean b/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Deriv.lean index 05cec5ab..34266d24 100644 --- a/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Deriv.lean +++ b/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Deriv.lean @@ -64,10 +64,7 @@ lemma _root_.HasFDerivAt.tendsto_bregDiv_slope_zero variable [OrderClosedTopology F] -/-- -For a convex function `f : E → F`, if `f` has a Fréchet derivative at `x` represented by the -continuous linear map `g`, then `g` is a subgradient of `f` at `x` over the set `V`. --/ +/-- A Fréchet derivative of a convex function is a subgradient. -/ lemma _root_.HasFDerivAt.mem_subdifferential (hderiv : HasFDerivAt f g x) (hf : ConvexOn ℝ V f) (hx : x ∈ V) : (g : E →+ F) ∈ ∂[V, x] f := by @@ -84,10 +81,6 @@ section Real variable {f : E → ℝ} {g h : E →L[ℝ] ℝ} -/-- -If `f : E → ℝ` has Fréchet derivative `g` at an interior point `x` of `V`, -then any continuous linear subgradient `h ∈ ∂[V, x] f` satisfies `h w ≤ g w` for all directions `w`. --/ lemma _root_.HasFDerivAt.le_of_mem_subdifferential (hderiv : HasFDerivAt f g x) (hV : V ∈ 𝓝 x) (hsub : (h : E →+ ℝ) ∈ ∂[V, x] f) (w : E) : h w ≤ g w := by @@ -100,10 +93,7 @@ lemma _root_.HasFDerivAt.le_of_mem_subdifferential inv_mul_cancel_left₀ ht_pos.ne'] using mul_le_mul_of_nonneg_left (sub_nonneg.mp (hsub.2 (x + t • w) ht_V)) (inv_nonneg.mpr ht_pos.le) -/-- -If `f : E → ℝ` has Fréchet derivative `g` at an interior point `x` of `V`, -then the subgradient is unique and equal to `g`. --/ +/-- Uniqueness of the subgradient at an interior differentiable point. -/ lemma _root_.HasFDerivAt.eq_of_mem_subdifferential (hderiv : HasFDerivAt f g x) (hV : V ∈ 𝓝 x) (hsub : (h : E →+ ℝ) ∈ ∂[V, x] f) : h = g := by From 15014afd2c9f7c3cf37eda37695322cd529e97a6 Mon Sep 17 00:00:00 2001 From: ISIPINK Date: Mon, 21 Sep 2026 16:38:19 +0200 Subject: [PATCH 09/15] changed from additive maps to continous linear maps --- .../ConvexAnalysis/Bregman/Basic.lean | 104 +++++++++------- .../ConvexAnalysis/Subgradient/Basic.lean | 112 ++++++++++-------- .../ConvexAnalysis/Subgradient/Deriv.lean | 29 ++--- 3 files changed, 137 insertions(+), 108 deletions(-) diff --git a/LeanMachineLearning/ForMathlib/ConvexAnalysis/Bregman/Basic.lean b/LeanMachineLearning/ForMathlib/ConvexAnalysis/Bregman/Basic.lean index d34f4e32..7cdb18d3 100644 --- a/LeanMachineLearning/ForMathlib/ConvexAnalysis/Bregman/Basic.lean +++ b/LeanMachineLearning/ForMathlib/ConvexAnalysis/Bregman/Basic.lean @@ -6,6 +6,7 @@ Authors: Isidoor Pinillo Esquivel module public import Mathlib.Analysis.Convex.Function +public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic public import Mathlib.Tactic /-! @@ -20,7 +21,7 @@ product rules, affine invariance, and convexity preservation. * `Analysis.Convex.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 - an additive map `J : E →+ F` (e.g. a derivative, gradient, or subgradient). + a continuous linear map `J : E →L[R] F` (e.g. a derivative, gradient, or subgradient). ## Notation @@ -31,11 +32,17 @@ product rules, affine invariance, and convexity preservation. namespace Analysis.Convex -variable {E F G : Type*} [AddCommGroup E] [AddCommGroup F] [AddCommGroup G] +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 additive mapping `E →+ F`. -/ -def bregDiv (f : E → F) (x y : E) (J : E →+ F) : F := +`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`. -/ @@ -50,85 +57,87 @@ meta def unexpandBregDiv : Lean.PrettyPrinter.Unexpander | _ => throw () @[simp] -lemma bregDiv_self (f : E → F) (x : E) (J_x : E →+ F) : +lemma bregDiv_self : D_[f](x, x, J_x) = 0 := by simp [bregDiv] -lemma bregDiv_three_point (f : E → F) (x y z : E) (J_x J_y : E →+ F) : +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, AddMonoidHom.sub_apply] + simp only [bregDiv, map_sub, sub_apply] abel -lemma bregDiv_add_swap (f : E → F) (x y : E) (J_x J_y : E →+ F) : +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, AddMonoidHom.sub_apply] + simp only [bregDiv, map_sub, sub_apply] abel -lemma bregDiv_fun_bregDiv (f : E → F) (x y z : E) (J_x J_y : E →+ F) : +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, AddMonoidHom.sub_apply] + simp only [bregDiv, map_sub, sub_apply] abel -lemma bregDiv_add (f₁ f₂ : E → F) (x y : E) (J₁ J₂ : E →+ F) : +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, AddMonoidHom.add_apply, map_sub] + simp only [bregDiv, Pi.add_apply, add_apply, map_sub] abel -lemma bregDiv_prod {E₁ E₂ : Type*} [AddCommGroup E₁] [AddCommGroup E₂] - (f₁ : E₁ → F) (f₂ : E₂ → F) (x y : E₁ × E₂) (J₁ : E₁ →+ F) (J₂ : E₂ →+ F) : +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, AddMonoidHom.coprod_apply, map_sub] + simp only [bregDiv, ContinuousLinearMap.coprod_apply, map_sub] abel @[simp] -lemma bregDiv_const (c : F) (x y : E) : - D_[fun _ ↦ c](x, y, 0) = 0 := by +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 →+ F) (x y : E) : +lemma bregDiv_linear (h : E →L[R] F) : D_[h](x, y, h) = 0 := by simp [bregDiv] @[simp] -lemma bregDiv_add_const (f : E → F) (c : F) (x y : E) (J : E →+ F) : +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) (f : E → F) (x y : E) (J : E →+ F) : +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 (f : E → F) (h : E →+ F) (x y : E) (J : E →+ F) : +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, AddMonoidHom.add_apply, map_sub] + simp only [bregDiv, add_apply, map_sub] abel @[simp] -lemma bregDiv_neg (f : E → F) (x y : E) (J : E →+ F) : +lemma bregDiv_neg [IsTopologicalAddGroup F] : D_[-f](x, y, -J) = - D_[f](x, y, J) := by - simp only [bregDiv, Pi.neg_apply, AddMonoidHom.neg_apply, map_sub] + simp only [bregDiv, Pi.neg_apply, neg_apply, map_sub] abel -lemma bregDiv_comp_neg (f : E → F) (x y : E) (J : E →+ F) : +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_translate (f : E → F) (x₀ : E) (x y : E) (J : E →+ F) : +lemma bregDiv_translate (x₀ : E) : D_[fun z ↦ f (z + x₀)](x, y, J) = D_[f](x + x₀, y + x₀, J) := by simp [bregDiv] section ChainRules -lemma bregDiv_comp_affine {E₁ : Type*} [AddCommGroup E₁] - (f : E → F) (A : E₁ →+ E) (b : E) (x y : E₁) (J : E →+ F) : +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 (f₂ : F → G) (f₁ : E → F) (x y : E) (J₂ : F →+ G) (J₁ : E →+ F) : +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] @@ -136,25 +145,26 @@ end ChainRules section CommRing -variable {R : Type*} [CommRing R] +variable {R' : Type*} [CommRing R'] [TopologicalSpace R'] [IsTopologicalAddGroup R'] + [ContinuousSMul R' R'] [Module R' E] /-- First-order product rule for Bregman divergences. -/ -lemma bregDiv_mul (f₁ f₂ : E → R) (x y : E) (J₁ J₂ : E →+ R) : +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, AddMonoidHom.add_apply, AddMonoidHom.smul_apply, map_sub, smul_eq_mul] + simp only [Pi.mul_apply, add_apply, smul_apply, map_sub, smul_eq_mul] ring - end CommRing section Order -variable {F' : Type*} [AddCommGroup F'] [Preorder F'] [AddRightMono F'] +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 →+ 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] @@ -163,13 +173,15 @@ end Order section Module -variable {R : Type*} [CommRing R] [Module R F] +variable {R' : Type*} [CommRing R'] [Module R' E] [Module R' F] + [ContinuousAdd F] [ContinuousConstSMul R' F] -lemma bregDiv_smul (c : R) (f : E → F) (x y : E) (J : E →+ F) : +omit [ContinuousAdd F] in +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 (f : E → F) (x y : E) (J₁ J₂ : E →+ F) (w : R) : +lemma bregDiv_convexCombination (f : E → F) (x y : E) (J₁ J₂ : E →L[R'] F) (w : R') : D_[f](x, y, w • J₁ + (1 - w) • J₂) = w • D_[f](x, y, J₁) + (1 - w) • D_[f](x, y, J₂) := by calc D_[f](x, y, w • J₁ + (1 - w) • J₂) @@ -184,13 +196,15 @@ end Module section Convexity -variable {𝕜 E' F' : Type*} [Semiring 𝕜] [PartialOrder 𝕜] -variable [AddCommGroup E'] [Module 𝕜 E'] -variable [AddCommGroup F'] [Module 𝕜 F'] [PartialOrder F'] [IsOrderedAddMonoid F'] +variable {𝕜 E' F' : Type*} [Ring 𝕜] [PartialOrder 𝕜] +variable [AddCommGroup E'] [Module 𝕜 E'] [TopologicalSpace E'] +variable [AddCommGroup F'] [Module 𝕜 F'] [TopologicalSpace F'] + [PartialOrder F'] [IsOrderedAddMonoid F'] -/-- If `f` is convex on `s`, then `x ↦ D_[f](x, y, J)` is convex on `s` for any linear map `J`. -/ +/-- If `f` is convex on `s`, then `x ↦ D_[f](x, y, J)` is convex on `s` for any +continuous linear map `J`. -/ lemma _root_.ConvexOn.bregDiv {s : Set E'} {f : E' → F'} (hf : ConvexOn 𝕜 s f) - (J : E' →ₗ[𝕜] F') (y : E') : + (J : E' →L[𝕜] F') (y : E') : ConvexOn 𝕜 s (fun x ↦ D_[f](x, y, J)) := by simp only [Analysis.Convex.bregDiv, sub_eq_add_neg, map_add, map_neg, neg_add_rev, neg_neg] apply ConvexOn.add @@ -199,7 +213,7 @@ lemma _root_.ConvexOn.bregDiv {s : Set E'} {f : E' → F'} (hf : ConvexOn 𝕜 s · exact convexOn_const (-f y) hf.1 · apply ConvexOn.add · exact convexOn_const (J y) hf.1 - · exact (-J).convexOn hf.1 + · exact (-J.toLinearMap).convexOn hf.1 end Convexity diff --git a/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Basic.lean b/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Basic.lean index c8774fca..2627c2af 100644 --- a/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Basic.lean +++ b/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Basic.lean @@ -8,6 +8,7 @@ module public import LeanMachineLearning.ForMathlib.ConvexAnalysis.Bregman.Basic public import Mathlib.Analysis.Convex.Function public import Mathlib.Order.ConditionallyCompleteLattice.Basic +public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic public import Mathlib.Tactic /-! @@ -22,7 +23,8 @@ while supporting constrained convex analysis. ## Main definitions -* `Analysis.Convex.IsSubgradient V f y g_y`: `g_y : E →+ F` is a subgradient of `f` at `y` on `V`. +* `Analysis.Convex.IsSubgradient V f y g_y`: `g_y : E →L[R] F` is a subgradient of `f` + at `y` on `V`. * `Analysis.Convex.subdifferential V f y`: The subdifferential set `∂[V, y] f`. ## Main results @@ -45,14 +47,19 @@ namespace Analysis.Convex open scoped Bregman -variable {E F : Type*} [AddCommGroup E] [AddCommGroup F] [Preorder F] +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_y` is a subgradient of `f` at `y` on domain `V` (non-negativity of Bregman divergence). -/ -def IsSubgradient (V : Set E) (f : E → F) (y : E) (g_y : E →+ F) : Prop := +def IsSubgradient (V : Set E) (f : E → F) (y : E) (g_y : E →L[R] F) : Prop := y ∈ V ∧ ∀ x ∈ V, 0 ≤ D_[f](x, y, g_y) /-- The subdifferential `∂[V, y] f` of `f` at `y` on `V`. -/ -def subdifferential (V : Set E) (f : E → F) (y : E) : Set (E →+ F) := +def subdifferential (V : Set E) (f : E → F) (y : E) : Set (E →L[R] F) := { g | IsSubgradient V f y g } /-- Scoped notation for `subdifferential`. -/ @@ -64,7 +71,7 @@ meta def unexpandSubdifferential : Lean.PrettyPrinter.Unexpander | `($_ $V $f $y) => `(∂[$V, $y] $f) | _ => throw () -variable {V : Set E} {f : E → F} {y x : E} {g_y : E →+ F} +variable {V : Set E} {f : E → F} {y x : E} {g_y : E →L[R] F} @[local simp] lemma mem_subdifferential_iff : @@ -72,10 +79,10 @@ lemma mem_subdifferential_iff : @[simp] lemma mem_subdifferential_const_iff {c : F} : - (0 : E →+ F) ∈ ∂[V, y] (fun _ ↦ c) ↔ y ∈ V := by simp + (0 : E →L[R] F) ∈ ∂[V, y] (fun _ ↦ c) ↔ y ∈ V := by simp @[simp] -lemma mem_subdifferential_linear_iff {h : E →+ F} : +lemma mem_subdifferential_linear_iff {h : E →L[R] F} : h ∈ ∂[V, y] h ↔ y ∈ V := by simp @[simp] @@ -87,32 +94,35 @@ lemma mem_subdifferential_const_add_iff {c : F} : g_y ∈ ∂[V, y] (fun x ↦ c + f x) ↔ g_y ∈ ∂[V, y] f := by simp @[simp] -lemma mem_subdifferential_add_linear_iff {h : E →+ F} : - (g_y + h) ∈ ∂[V, y] (fun x ↦ f x + h x) ↔ g_y ∈ ∂[V, y] f := by simp +lemma mem_subdifferential_add_linear_iff [ContinuousAdd F] {h : E →L[R] F} : + (g_y + h) ∈ ∂[V, y] (fun x ↦ f x + h x) ↔ g_y ∈ ∂[V, y] f := by + simp [bregDiv_add_linear] @[simp] -lemma mem_subdifferential_bregDiv_iff {g_x g_y : E →+ F} : +lemma mem_subdifferential_bregDiv_iff [IsTopologicalAddGroup F] {g_x g_y : E →L[R] F} : (g_x - g_y) ∈ ∂[V, x] (fun z ↦ D_[f](z, y, g_y)) ↔ g_x ∈ ∂[V, x] f := by simp [bregDiv_fun_bregDiv] lemma zero_mem_subdifferential_iff : - (0 : E →+ F) ∈ ∂[V, y] f ↔ y ∈ V ∧ ∀ x ∈ V, 0 ≤ f x - f y := by simp [bregDiv] + (0 : E →L[R] F) ∈ ∂[V, y] f ↔ y ∈ V ∧ ∀ x ∈ V, 0 ≤ f x - f y := by simp [bregDiv] -lemma IsSubgradient.comp_affine {E₁ : Type*} [AddCommGroup E₁] - {V₁ : Set E₁} {y₁ : E₁} {A : E₁ →+ E} {b : E} +lemma IsSubgradient.comp_affine + {V₁ : Set E₁} {y₁ : E₁} {A : E₁ →L[R] E} {b : E} (hy₁ : y₁ ∈ V₁) (h_map : ∀ x ∈ V₁, A x + b ∈ V) (h_sub : g_y ∈ ∂[V, A y₁ + b] f) : - (g_y.comp A) ∈ ∂[V₁, y₁] (fun x ↦ f (A x + b)) := - ⟨hy₁, fun x hx ↦ by simp [bregDiv_comp_affine, h_sub.2 (A x + b) (h_map x hx)]⟩ + (g_y.comp A) ∈ ∂[V₁, y₁] (fun x ↦ f (A x + b)) := by + simp only [mem_subdifferential_iff, bregDiv_comp_affine] at * + exact ⟨hy₁, fun x hx ↦ h_sub.2 (A x + b) (h_map x hx)⟩ /-- **Chain rule**: `g₂ ∘ g₁` is a subgradient of `f₂ ∘ f₁` when `g₂` is non-negative. -/ -lemma IsSubgradient.comp {G : Type*} [AddCommGroup G] [Preorder G] [IsOrderedAddMonoid G] - {f₂ : F → G} {f₁ : E → F} {g₂ : F →+ G} {g₁ : E →+ F} +lemma IsSubgradient.comp [Preorder G] [IsOrderedAddMonoid G] + {f₂ : F → G} {f₁ : E → F} {g₂ : F →L[R] G} {g₁ : E →L[R] F} (h₂ : g₂ ∈ ∂[f₁ '' V, f₁ y] f₂) (h₁ : g₁ ∈ ∂[V, y] f₁) (hg₂_nonneg : ∀ z ≥ 0, 0 ≤ g₂ z) : - (g₂.comp g₁) ∈ ∂[V, y] (f₂ ∘ f₁) := - ⟨h₁.1, fun x hx ↦ by - simp only [bregDiv_comp, add_nonneg (h₂.2 (f₁ x) ⟨x, hx, rfl⟩) (hg₂_nonneg _ (h₁.2 x hx))]⟩ + (g₂.comp g₁) ∈ ∂[V, y] (f₂ ∘ f₁) := by + refine ⟨h₁.1, fun x hx ↦ ?_⟩ + rw [bregDiv_comp] + exact add_nonneg (h₂.2 (f₁ x) ⟨x, hx, rfl⟩) (hg₂_nonneg _ (h₁.2 x hx)) section OrderedGroup @@ -123,77 +133,81 @@ lemma mem_subdifferential_iff_le : g_y ∈ ∂[V, y] f ↔ y ∈ V ∧ ∀ x ∈ V, f y + g_y (x - y) ≤ f x := by simp [bregDiv, sub_sub, sub_nonneg] -lemma IsSubgradient.monotonicity {g_x : E →+ F} +lemma IsSubgradient.monotonicity [IsTopologicalAddGroup F] {g_x : E →L[R] F} (hx_sub : g_x ∈ ∂[V, x] f) (hy_sub : g_y ∈ ∂[V, y] f) : 0 ≤ (g_x - g_y) (x - y) := by - rw [← bregDiv_add_swap f x y g_x g_y] + rw [← bregDiv_add_swap] exact add_nonneg (hx_sub.2 y hy_sub.1) (hy_sub.2 x hx_sub.1) - /-- **Fermat's rule**: `0` is a subgradient of `f` at `y` iff `y` is a minimizer of `f` on `V`. -/ lemma zero_mem_subdifferential_iff_isMinOn : - (0 : E →+ F) ∈ ∂[V, y] f ↔ y ∈ V ∧ IsMinOn f V y := by + (0 : E →L[R] F) ∈ ∂[V, y] f ↔ y ∈ V ∧ IsMinOn f V y := by simp [bregDiv, sub_nonneg, isMinOn_iff] -lemma IsSubgradient.add {f₁ f₂ : E → F} {g₁ g₂ : E →+ F} +lemma IsSubgradient.add [ContinuousAdd F] {f₁ f₂ : E → F} {g₁ g₂ : E →L[R] F} (h₁ : g₁ ∈ ∂[V, y] f₁) (h₂ : g₂ ∈ ∂[V, y] f₂) : - (g₁ + g₂) ∈ ∂[V, y] (f₁ + f₂) := - ⟨h₁.1, fun x hx ↦ by simp [bregDiv_add, add_nonneg (h₁.2 x hx) (h₂.2 x hx)]⟩ + (g₁ + g₂) ∈ ∂[V, y] (f₁ + f₂) := by + simp only [mem_subdifferential_iff, bregDiv_add] at * + exact ⟨h₁.1, fun x hx ↦ add_nonneg (h₁.2 x hx) (h₂.2 x hx)⟩ -lemma IsSubgradient.add_isMinOn {f₁ f₂ : E → F} {x : E} {g : E →+ F} +lemma IsSubgradient.add_isMinOn [ContinuousAdd F] {f₁ f₂ : E → F} {x : E} {g : E →L[R] F} (h_min : IsMinOn f₁ V x) (hx_mem : x ∈ V) (h_sub : g ∈ ∂[V, x] f₂) : g ∈ ∂[V, x] (f₁ + f₂) := by simpa using IsSubgradient.add (zero_mem_subdifferential_iff_isMinOn.mpr ⟨hx_mem, h_min⟩) h_sub -lemma IsSubgradient.of_le_of_eq {f₁ f₂ : E → F} {g_y : E →+ F} +end OrderedGroup + +lemma IsSubgradient.of_le_of_eq [AddRightMono F] {f₁ f₂ : E → F} {g_y : E →L[R] F} (h_sub : g_y ∈ ∂[V, y] f₁) (h_le : ∀ x ∈ V, f₁ x ≤ f₂ x) (h_eq : f₁ y = f₂ y) : g_y ∈ ∂[V, y] f₂ := ⟨h_sub.1, fun x hx ↦ le_trans (h_sub.2 x hx) (bregDiv_le_of_le_of_eq (h_le x hx) h_eq)⟩ -end OrderedGroup - section ModuleBasic -variable {R : Type*} [CommRing R] [PartialOrder R] [Module R F] [PosSMulMono R F] +variable {R' : Type*} [CommRing R'] [PartialOrder R'] + [Module R' E] [Module R' F] [ContinuousConstSMul R' F] [PosSMulMono R' F] -lemma IsSubgradient.smul {c : R} (hc : 0 ≤ c) {f : E → F} {g_y : E →+ F} +lemma IsSubgradient.smul {c : R'} (hc : 0 ≤ c) {f : E → F} {g_y : E →L[R'] F} (h_sub : g_y ∈ ∂[V, y] f) : - (c • g_y) ∈ ∂[V, y] (c • f) := - ⟨h_sub.1, fun x hx ↦ by simp [bregDiv_smul, smul_nonneg hc (h_sub.2 x hx)]⟩ + (c • g_y) ∈ ∂[V, y] (c • f) := by + simp only [mem_subdifferential_iff, bregDiv_smul] at * + exact ⟨h_sub.1, fun x hx ↦ smul_nonneg hc (h_sub.2 x hx)⟩ end ModuleBasic section Module -variable {R : Type*} [CommRing R] [PartialOrder R] [IsOrderedRing R] - [IsOrderedAddMonoid F] [Module R F] [PosSMulMono R F] +variable {R' : Type*} [CommRing R'] [PartialOrder R'] [IsOrderedRing R'] + [Module R' E] [IsOrderedAddMonoid F] [Module R' F] [ContinuousConstSMul R' F] [PosSMulMono R' F] + [ContinuousAdd F] -lemma IsSubgradient.convexCombination {f : E → F} {g₁ g₂ : E →+ F} - (h₁ : g₁ ∈ ∂[V, y] f) (h₂ : g₂ ∈ ∂[V, y] f) {w : R} (hw : w ∈ Set.Icc (0 : R) 1) : - (w • g₁ + (1 - w) • g₂) ∈ ∂[V, y] f := - ⟨h₁.1, fun x hx ↦ by - simp [bregDiv_convexCombination, hw.1, sub_nonneg.mpr hw.2, - h₁.2 x hx, h₂.2 x hx, smul_nonneg, add_nonneg]⟩ +lemma IsSubgradient.convexCombination {f : E → F} {g₁ g₂ : E →L[R'] F} + (h₁ : g₁ ∈ ∂[V, y] f) (h₂ : g₂ ∈ ∂[V, y] f) {w : R'} (hw : w ∈ Set.Icc (0 : R') 1) : + (w • g₁ + (1 - w) • g₂) ∈ ∂[V, y] f := by + simp only [mem_subdifferential_iff, bregDiv_convexCombination] at * + exact ⟨h₁.1, fun x hx ↦ add_nonneg (smul_nonneg hw.1 (h₁.2 x hx)) + (smul_nonneg (sub_nonneg.mpr hw.2) (h₂.2 x hx))⟩ end Module section LinearOrder -variable {F_lin : Type*} [AddCommGroup F_lin] [LinearOrder F_lin] [IsOrderedAddMonoid F_lin] +variable {F_lin : Type*} [AddCommGroup F_lin] [Module R F_lin] [TopologicalSpace F_lin] + [LinearOrder F_lin] [IsOrderedAddMonoid F_lin] -lemma IsSubgradient.max_left {f₁ f₂ : E → F_lin} {g_y : E →+ F_lin} +lemma IsSubgradient.max_left {f₁ f₂ : E → F_lin} {g_y : E →L[R] F_lin} (h_sub : g_y ∈ ∂[V, y] f₁) (h_active : f₁ y = max (f₁ y) (f₂ y)) : g_y ∈ ∂[V, y] (fun x ↦ max (f₁ x) (f₂ x)) := IsSubgradient.of_le_of_eq h_sub (fun x _ ↦ le_max_left (f₁ x) (f₂ x)) h_active -lemma IsSubgradient.max_right {f₁ f₂ : E → F_lin} {g_y : E →+ F_lin} +lemma IsSubgradient.max_right {f₁ f₂ : E → F_lin} {g_y : E →L[R] F_lin} (h_sub : g_y ∈ ∂[V, y] f₂) (h_active : f₂ y = max (f₁ y) (f₂ y)) : g_y ∈ ∂[V, y] (fun x ↦ max (f₁ x) (f₂ x)) := IsSubgradient.of_le_of_eq h_sub (fun x _ ↦ le_max_right (f₁ x) (f₂ x)) h_active lemma IsSubgradient.finset_sup {ι : Type*} {s : Finset ι} - {f_i : ι → E → F_lin} {i : ι} {g_y : E →+ F_lin} + {f_i : ι → E → F_lin} {i : ι} {g_y : E →L[R] F_lin} (his : i ∈ s) (h_sub : g_y ∈ ∂[V, y] (f_i i)) (h_active : f_i i y = s.sup' ⟨i, his⟩ (fun j ↦ f_i j y)) : g_y ∈ ∂[V, y] (fun x ↦ s.sup' ⟨i, his⟩ (fun j ↦ f_i j x)) := @@ -203,10 +217,10 @@ end LinearOrder section Lattice -variable {F_lat : Type*} [AddCommGroup F_lat] +variable {F_lat : Type*} [AddCommGroup F_lat] [Module R F_lat] [TopologicalSpace F_lat] [ConditionallyCompleteLattice F_lat] [IsOrderedAddMonoid F_lat] -lemma IsSubgradient.ciSup {ι : Type*} {f_i : ι → E → F_lat} {i : ι} {g_y : E →+ F_lat} +lemma IsSubgradient.ciSup {ι : Type*} {f_i : ι → E → F_lat} {i : ι} {g_y : E →L[R] F_lat} (h_sub : g_y ∈ ∂[V, y] (f_i i)) (h_active : f_i i y = ⨆ j, f_i j y) (h_bdd : ∀ x ∈ V, BddAbove (Set.range (fun j ↦ f_i j x))) : diff --git a/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Deriv.lean b/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Deriv.lean index 34266d24..bcf1671e 100644 --- a/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Deriv.lean +++ b/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Deriv.lean @@ -41,7 +41,7 @@ open Asymptotics Filter /-- Scaled Bregman divergence monotonicity along segments for convex functions. -/ lemma _root_.ConvexOn.bregDiv_slope_le (hf : ConvexOn ℝ V f) - {z : E} (hx : x ∈ V) (hz : z ∈ V) (J : E →ₗ[ℝ] F) + {z : E} (hx : x ∈ V) (hz : z ∈ V) (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 @@ -55,7 +55,7 @@ omit [PartialOrder F] [IsOrderedAddMonoid F] [PosSMulMono ℝ F] in scaled by `t⁻¹` converges to `0`. -/ lemma _root_.HasFDerivAt.tendsto_bregDiv_slope_zero (hderiv : HasFDerivAt f g x) (w : E) : - Tendsto (fun t : ℝ ↦ t⁻¹ • D_[f](x + t • w, x, (g : E →+ F))) (𝓝[>] 0) (𝓝 0) := by + 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' ?_ @@ -67,14 +67,14 @@ variable [OrderClosedTopology F] /-- A Fréchet derivative of a convex function is a subgradient. -/ lemma _root_.HasFDerivAt.mem_subdifferential (hderiv : HasFDerivAt f g x) (hf : ConvexOn ℝ V f) (hx : x ∈ V) : - (g : E →+ F) ∈ ∂[V, x] f := by + g ∈ ∂[V, x] f := by refine ⟨hx, fun z hz ↦ le_of_tendsto (hderiv.tendsto_bregDiv_slope_zero (z - x)) ?_⟩ 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.toLinearMap ht0 ht1 + with t (ht0 : 0 < t) ht1 using hf.bregDiv_slope_le hx hz g ht0 ht1 lemma subgradient_of_hasFDerivAt (hf : ConvexOn ℝ V f) (hx : x ∈ V) (hderiv : HasFDerivAt f g x) : - (g : E →+ F) ∈ ∂[V, x] f := + g ∈ ∂[V, x] f := hderiv.mem_subdifferential hf hx section Real @@ -82,7 +82,7 @@ section Real variable {f : E → ℝ} {g h : E →L[ℝ] ℝ} lemma _root_.HasFDerivAt.le_of_mem_subdifferential - (hderiv : HasFDerivAt f g x) (hV : V ∈ 𝓝 x) (hsub : (h : E →+ ℝ) ∈ ∂[V, x] f) (w : E) : + (hderiv : HasFDerivAt f g x) (hV : V ∈ 𝓝 x) (hsub : h ∈ ∂[V, x] f) (w : E) : h w ≤ g w := by have h_nhds : (fun t : ℝ ↦ x + t • w) ⁻¹' V ∈ 𝓝 0 := (continuous_const.add (continuous_id'.smul continuous_const)).continuousAt.preimage_mem_nhds @@ -95,7 +95,7 @@ lemma _root_.HasFDerivAt.le_of_mem_subdifferential /-- Uniqueness of the subgradient at an interior differentiable point. -/ lemma _root_.HasFDerivAt.eq_of_mem_subdifferential - (hderiv : HasFDerivAt f g x) (hV : V ∈ 𝓝 x) (hsub : (h : E →+ ℝ) ∈ ∂[V, x] f) : + (hderiv : HasFDerivAt f g x) (hV : V ∈ 𝓝 x) (hsub : h ∈ ∂[V, x] f) : h = g := by ext v exact le_antisymm (hderiv.le_of_mem_subdifferential hV hsub v) @@ -109,20 +109,21 @@ and `f₂` is convex on `V`: `g` is a subgradient of `f₁ + f₂` at `x` if and lemma _root_.HasFDerivAt.mem_subdifferential_add_iff {f₁ f₂ : E → ℝ} {g₁ g : E →L[ℝ] ℝ} (hderiv₁ : HasFDerivAt f₁ g₁ x) (hf₁ : ConvexOn ℝ V f₁) (hf₂ : ConvexOn ℝ V f₂) (hx : x ∈ V) : - (g : E →+ ℝ) ∈ ∂[V, x] (f₁ + f₂) ↔ (g - g₁ : E →+ ℝ) ∈ ∂[V, x] f₂ := by - have h_eq : (g : E →+ ℝ) = (g₁ : E →+ ℝ) + (g - g₁ : E →+ ℝ) := by ext; simp + g ∈ ∂[V, x] (f₁ + f₂) ↔ (g - g₁) ∈ ∂[V, x] f₂ := by + have h_eq : g = g₁ + (g - g₁) := by ext; simp constructor · rintro ⟨-, hg⟩ refine ⟨hx, fun z hz ↦ 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_slope : t⁻¹ • D_[f₂](x + t • (z - x), x, (g - g₁ : E →+ ℝ)) ≤ - D_[f₂](z, x, (g - g₁ : E →+ ℝ)) := - hf₂.bregDiv_slope_le hx hz (g - g₁).toLinearMap ht0 ht1 + have h_slope : t⁻¹ • D_[f₂](x + t • (z - x), x, g - g₁) ≤ + D_[f₂](z, x, g - g₁) := + hf₂.bregDiv_slope_le hx hz (g - g₁) ht0 ht1 have h_nonneg := smul_nonneg (inv_nonneg.mpr ht0.le) (hg _ (hf₂.1.add_smul_sub_mem hx hz ⟨ht0.le, ht1⟩)) - rw [h_eq, bregDiv_add, smul_add] at h_nonneg + have h_lin : g = g₁ + (g - g₁) := by ext; simp + rw [h_lin, bregDiv_add, smul_add] at h_nonneg dsimp at * linarith · intro h₂ @@ -133,7 +134,7 @@ lemma mem_subdifferential_add_hasFDerivAt_iff {f₁ f₂ : E → ℝ} {g₁ g : E →L[ℝ] ℝ} (hf₁ : ConvexOn ℝ V f₁) (hf₂ : ConvexOn ℝ V f₂) (hx : x ∈ V) (hderiv₁ : HasFDerivAt f₁ g₁ x) : - (g : E →+ ℝ) ∈ ∂[V, x] (f₁ + f₂) ↔ (g - g₁ : E →+ ℝ) ∈ ∂[V, x] f₂ := + g ∈ ∂[V, x] (f₁ + f₂) ↔ (g - g₁) ∈ ∂[V, x] f₂ := hderiv₁.mem_subdifferential_add_iff hf₁ hf₂ hx end Real From 3fc8c3765d741ce7eba939e2cb448572202c7643 Mon Sep 17 00:00:00 2001 From: ISIPINK Date: Mon, 21 Sep 2026 16:40:13 +0200 Subject: [PATCH 10/15] removed unexpanders --- .../ForMathlib/ConvexAnalysis/Bregman/Basic.lean | 6 ------ .../ForMathlib/ConvexAnalysis/Subgradient/Basic.lean | 6 ------ 2 files changed, 12 deletions(-) diff --git a/LeanMachineLearning/ForMathlib/ConvexAnalysis/Bregman/Basic.lean b/LeanMachineLearning/ForMathlib/ConvexAnalysis/Bregman/Basic.lean index 7cdb18d3..11838999 100644 --- a/LeanMachineLearning/ForMathlib/ConvexAnalysis/Bregman/Basic.lean +++ b/LeanMachineLearning/ForMathlib/ConvexAnalysis/Bregman/Basic.lean @@ -50,12 +50,6 @@ scoped[Bregman] notation "D_[" f "](" x ", " y ", " J ")" => Analysis.Convex.bre open scoped Bregman -/-- Unexpander for `bregDiv`. -/ -@[app_unexpander bregDiv] -meta def unexpandBregDiv : Lean.PrettyPrinter.Unexpander - | `($_ $f $x $y $J) => `(D_[$f]($x, $y, $J)) - | _ => throw () - @[simp] lemma bregDiv_self : D_[f](x, x, J_x) = 0 := by diff --git a/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Basic.lean b/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Basic.lean index 2627c2af..a0e7f86d 100644 --- a/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Basic.lean +++ b/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Basic.lean @@ -65,12 +65,6 @@ def subdifferential (V : Set E) (f : E → F) (y : E) : Set (E →L[R] F) := /-- Scoped notation for `subdifferential`. -/ scoped[Bregman] notation:60 "∂[" V ", " y "] " f:50 => Analysis.Convex.subdifferential V f y -/-- Unexpander for `subdifferential`. -/ -@[app_unexpander subdifferential] -meta def unexpandSubdifferential : Lean.PrettyPrinter.Unexpander - | `($_ $V $f $y) => `(∂[$V, $y] $f) - | _ => throw () - variable {V : Set E} {f : E → F} {y x : E} {g_y : E →L[R] F} @[local simp] From 723f1698f90610115cac3121950b21e1da3eac17 Mon Sep 17 00:00:00 2001 From: ISIPINK Date: Mon, 21 Sep 2026 17:03:15 +0200 Subject: [PATCH 11/15] changed membership to predicate for issubgradient --- .../ConvexAnalysis/Subgradient/Basic.lean | 141 +++++++++--------- .../ConvexAnalysis/Subgradient/Deriv.lean | 55 +++---- 2 files changed, 101 insertions(+), 95 deletions(-) diff --git a/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Basic.lean b/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Basic.lean index a0e7f86d..74db61fd 100644 --- a/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Basic.lean +++ b/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Basic.lean @@ -30,8 +30,8 @@ while supporting constrained convex analysis. ## Main results * Chain rules: `Analysis.Convex.IsSubgradient.comp_affine` and `Analysis.Convex.IsSubgradient.comp`. -* Equivalence with classical inequality: `Analysis.Convex.mem_subdifferential_iff_le`. -* Fermat's rule: `Analysis.Convex.zero_mem_subdifferential_iff_isMinOn`. +* Equivalence with classical inequality: `Analysis.Convex.isSubgradient_iff_le`. +* Fermat's rule: `Analysis.Convex.isSubgradient_zero_iff_isMinOn`. * Suprema and maxima: `Analysis.Convex.IsSubgradient.max_left`, `Analysis.Convex.IsSubgradient.max_right`, `Analysis.Convex.IsSubgradient.finset_sup`, and `Analysis.Convex.IsSubgradient.ciSup`. @@ -56,7 +56,7 @@ variable {R E E₁ F G : Type*} [Ring R] /-- `g_y` is a subgradient of `f` at `y` on domain `V` (non-negativity of Bregman divergence). -/ def IsSubgradient (V : Set E) (f : E → F) (y : E) (g_y : E →L[R] F) : Prop := - y ∈ V ∧ ∀ x ∈ V, 0 ≤ D_[f](x, y, g_y) + ∀ x ∈ V, 0 ≤ D_[f](x, y, g_y) /-- The subdifferential `∂[V, y] f` of `f` at `y` on `V`. -/ def subdifferential (V : Set E) (f : E → F) (y : E) : Set (E →L[R] F) := @@ -67,95 +67,98 @@ scoped[Bregman] notation:60 "∂[" V ", " y "] " f:50 => Analysis.Convex.subdiff variable {V : Set E} {f : E → F} {y x : E} {g_y : E →L[R] F} -@[local simp] +@[simp] lemma mem_subdifferential_iff : - g_y ∈ ∂[V, y] f ↔ y ∈ V ∧ ∀ x ∈ V, 0 ≤ D_[f](x, y, g_y) := Iff.rfl + g_y ∈ ∂[V, y] f ↔ IsSubgradient V f y g_y := Iff.rfl -@[simp] -lemma mem_subdifferential_const_iff {c : F} : - (0 : E →L[R] F) ∈ ∂[V, y] (fun _ ↦ c) ↔ y ∈ V := by simp +lemma isSubgradient_const (c : F) : + IsSubgradient V (fun _ ↦ c) y (0 : E →L[R] F) := by + simp [IsSubgradient] @[simp] -lemma mem_subdifferential_linear_iff {h : E →L[R] F} : - h ∈ ∂[V, y] h ↔ y ∈ V := by simp +lemma isSubgradient_linear (h : E →L[R] F) : + IsSubgradient V h y h := by + simp [IsSubgradient] @[simp] -lemma mem_subdifferential_add_const_iff {c : F} : - g_y ∈ ∂[V, y] (fun x ↦ f x + c) ↔ g_y ∈ ∂[V, y] f := by simp +lemma isSubgradient_add_const_iff {c : F} : + IsSubgradient V (fun x ↦ f x + c) y g_y ↔ IsSubgradient V f y g_y := by + simp [IsSubgradient, bregDiv] @[simp] -lemma mem_subdifferential_const_add_iff {c : F} : - g_y ∈ ∂[V, y] (fun x ↦ c + f x) ↔ g_y ∈ ∂[V, y] f := by simp +lemma isSubgradient_const_add_iff {c : F} : + IsSubgradient V (fun x ↦ c + f x) y g_y ↔ IsSubgradient V f y g_y := by + simp [IsSubgradient, bregDiv] @[simp] -lemma mem_subdifferential_add_linear_iff [ContinuousAdd F] {h : E →L[R] F} : - (g_y + h) ∈ ∂[V, y] (fun x ↦ f x + h x) ↔ g_y ∈ ∂[V, y] f := by - simp [bregDiv_add_linear] +lemma isSubgradient_add_linear_iff [ContinuousAdd F] {h : E →L[R] F} : + IsSubgradient V (fun x ↦ f x + h x) y (g_y + h) ↔ IsSubgradient V f y g_y := by + simp [IsSubgradient, bregDiv_add_linear] @[simp] -lemma mem_subdifferential_bregDiv_iff [IsTopologicalAddGroup F] {g_x g_y : E →L[R] F} : - (g_x - g_y) ∈ ∂[V, x] (fun z ↦ D_[f](z, y, g_y)) ↔ g_x ∈ ∂[V, x] f := by - simp [bregDiv_fun_bregDiv] +lemma isSubgradient_bregDiv_iff [IsTopologicalAddGroup F] {g_x g_y : E →L[R] F} : + IsSubgradient V (fun z ↦ D_[f](z, y, g_y)) x (g_x - g_y) ↔ IsSubgradient V f x g_x := by + simp [IsSubgradient, bregDiv_fun_bregDiv] -lemma zero_mem_subdifferential_iff : - (0 : E →L[R] F) ∈ ∂[V, y] f ↔ y ∈ V ∧ ∀ x ∈ V, 0 ≤ f x - f y := by simp [bregDiv] +lemma isSubgradient_zero_iff : + IsSubgradient V f y (0 : E →L[R] F) ↔ ∀ x ∈ V, 0 ≤ f x - f y := by + simp [IsSubgradient, bregDiv] lemma IsSubgradient.comp_affine {V₁ : Set E₁} {y₁ : E₁} {A : E₁ →L[R] E} {b : E} - (hy₁ : y₁ ∈ V₁) (h_map : ∀ x ∈ V₁, A x + b ∈ V) - (h_sub : g_y ∈ ∂[V, A y₁ + b] f) : - (g_y.comp A) ∈ ∂[V₁, y₁] (fun x ↦ f (A x + b)) := by - simp only [mem_subdifferential_iff, bregDiv_comp_affine] at * - exact ⟨hy₁, fun x hx ↦ h_sub.2 (A x + b) (h_map x hx)⟩ + (h_map : ∀ x ∈ V₁, A x + b ∈ V) + (h_sub : IsSubgradient V f (A y₁ + b) g_y) : + IsSubgradient V₁ (fun x ↦ f (A x + b)) y₁ (g_y.comp A) := fun x hx ↦ by + rw [bregDiv_comp_affine] + exact h_sub (A x + b) (h_map x hx) /-- **Chain rule**: `g₂ ∘ g₁` is a subgradient of `f₂ ∘ f₁` when `g₂` is non-negative. -/ lemma IsSubgradient.comp [Preorder G] [IsOrderedAddMonoid G] {f₂ : F → G} {f₁ : E → F} {g₂ : F →L[R] G} {g₁ : E →L[R] F} - (h₂ : g₂ ∈ ∂[f₁ '' V, f₁ y] f₂) (h₁ : g₁ ∈ ∂[V, y] f₁) + (h₂ : IsSubgradient (f₁ '' V) f₂ (f₁ y) g₂) (h₁ : IsSubgradient V f₁ y g₁) (hg₂_nonneg : ∀ z ≥ 0, 0 ≤ g₂ z) : - (g₂.comp g₁) ∈ ∂[V, y] (f₂ ∘ f₁) := by - refine ⟨h₁.1, fun x hx ↦ ?_⟩ + IsSubgradient V (f₂ ∘ f₁) y (g₂.comp g₁) := fun x hx ↦ by rw [bregDiv_comp] - exact add_nonneg (h₂.2 (f₁ x) ⟨x, hx, rfl⟩) (hg₂_nonneg _ (h₁.2 x hx)) + exact add_nonneg (h₂ (f₁ x) ⟨x, hx, rfl⟩) (hg₂_nonneg _ (h₁ x hx)) section OrderedGroup variable [IsOrderedAddMonoid F] /-- Equivalence with the classical definition. -/ -lemma mem_subdifferential_iff_le : - g_y ∈ ∂[V, y] f ↔ y ∈ V ∧ ∀ x ∈ V, f y + g_y (x - y) ≤ f x := by - simp [bregDiv, sub_sub, sub_nonneg] +lemma isSubgradient_iff_le : + IsSubgradient V f y g_y ↔ ∀ x ∈ V, f y + g_y (x - y) ≤ f x := by + simp [IsSubgradient, bregDiv, sub_sub, sub_nonneg] lemma IsSubgradient.monotonicity [IsTopologicalAddGroup F] {g_x : E →L[R] F} - (hx_sub : g_x ∈ ∂[V, x] f) (hy_sub : g_y ∈ ∂[V, y] f) : + (hx : x ∈ V) (hy : y ∈ V) + (hx_sub : IsSubgradient V f x g_x) (hy_sub : IsSubgradient V f y g_y) : 0 ≤ (g_x - g_y) (x - y) := by rw [← bregDiv_add_swap] - exact add_nonneg (hx_sub.2 y hy_sub.1) (hy_sub.2 x hx_sub.1) + exact add_nonneg (hx_sub y hy) (hy_sub x hx) -/-- **Fermat's rule**: `0` is a subgradient of `f` at `y` iff `y` is a minimizer of `f` on `V`. -/ -lemma zero_mem_subdifferential_iff_isMinOn : - (0 : E →L[R] F) ∈ ∂[V, y] f ↔ y ∈ V ∧ IsMinOn f V y := by - simp [bregDiv, sub_nonneg, isMinOn_iff] +lemma isSubgradient_zero_iff_isMinOn : + IsSubgradient V f y (0 : E →L[R] F) ↔ IsMinOn f V y := by + simp [IsSubgradient, bregDiv, sub_nonneg, isMinOn_iff] lemma IsSubgradient.add [ContinuousAdd F] {f₁ f₂ : E → F} {g₁ g₂ : E →L[R] F} - (h₁ : g₁ ∈ ∂[V, y] f₁) (h₂ : g₂ ∈ ∂[V, y] f₂) : - (g₁ + g₂) ∈ ∂[V, y] (f₁ + f₂) := by - simp only [mem_subdifferential_iff, bregDiv_add] at * - exact ⟨h₁.1, fun x hx ↦ add_nonneg (h₁.2 x hx) (h₂.2 x hx)⟩ + (h₁ : IsSubgradient V f₁ y g₁) (h₂ : IsSubgradient V f₂ y g₂) : + IsSubgradient V (f₁ + f₂) y (g₁ + g₂) := fun x hx ↦ by + rw [bregDiv_add] + exact add_nonneg (h₁ x hx) (h₂ x hx) lemma IsSubgradient.add_isMinOn [ContinuousAdd F] {f₁ f₂ : E → F} {x : E} {g : E →L[R] F} - (h_min : IsMinOn f₁ V x) (hx_mem : x ∈ V) (h_sub : g ∈ ∂[V, x] f₂) : - g ∈ ∂[V, x] (f₁ + f₂) := by - simpa using IsSubgradient.add (zero_mem_subdifferential_iff_isMinOn.mpr ⟨hx_mem, h_min⟩) h_sub + (h_min : IsMinOn f₁ V x) (h_sub : IsSubgradient V f₂ x g) : + IsSubgradient V (f₁ + f₂) x g := by + simpa using IsSubgradient.add (isSubgradient_zero_iff_isMinOn.mpr h_min) h_sub end OrderedGroup lemma IsSubgradient.of_le_of_eq [AddRightMono F] {f₁ f₂ : E → F} {g_y : E →L[R] F} - (h_sub : g_y ∈ ∂[V, y] f₁) (h_le : ∀ x ∈ V, f₁ x ≤ f₂ x) (h_eq : f₁ y = f₂ y) : - g_y ∈ ∂[V, y] f₂ := - ⟨h_sub.1, fun x hx ↦ le_trans (h_sub.2 x hx) - (bregDiv_le_of_le_of_eq (h_le x hx) h_eq)⟩ + (h_sub : IsSubgradient V f₁ y g_y) (h_le : ∀ x ∈ V, f₁ x ≤ f₂ x) (h_eq : f₁ y = f₂ y) : + IsSubgradient V f₂ y g_y := + fun x hx ↦ le_trans (h_sub x hx) + (bregDiv_le_of_le_of_eq (h_le x hx) h_eq) section ModuleBasic @@ -163,10 +166,10 @@ variable {R' : Type*} [CommRing R'] [PartialOrder R'] [Module R' E] [Module R' F] [ContinuousConstSMul R' F] [PosSMulMono R' F] lemma IsSubgradient.smul {c : R'} (hc : 0 ≤ c) {f : E → F} {g_y : E →L[R'] F} - (h_sub : g_y ∈ ∂[V, y] f) : - (c • g_y) ∈ ∂[V, y] (c • f) := by - simp only [mem_subdifferential_iff, bregDiv_smul] at * - exact ⟨h_sub.1, fun x hx ↦ smul_nonneg hc (h_sub.2 x hx)⟩ + (h_sub : IsSubgradient V f y g_y) : + IsSubgradient V (c • f) y (c • g_y) := fun x hx ↦ by + rw [bregDiv_smul] + exact smul_nonneg hc (h_sub x hx) end ModuleBasic @@ -177,11 +180,12 @@ variable {R' : Type*} [CommRing R'] [PartialOrder R'] [IsOrderedRing R'] [ContinuousAdd F] lemma IsSubgradient.convexCombination {f : E → F} {g₁ g₂ : E →L[R'] F} - (h₁ : g₁ ∈ ∂[V, y] f) (h₂ : g₂ ∈ ∂[V, y] f) {w : R'} (hw : w ∈ Set.Icc (0 : R') 1) : - (w • g₁ + (1 - w) • g₂) ∈ ∂[V, y] f := by - simp only [mem_subdifferential_iff, bregDiv_convexCombination] at * - exact ⟨h₁.1, fun x hx ↦ add_nonneg (smul_nonneg hw.1 (h₁.2 x hx)) - (smul_nonneg (sub_nonneg.mpr hw.2) (h₂.2 x hx))⟩ + (h₁ : IsSubgradient V f y g₁) (h₂ : IsSubgradient V f y g₂) + {w : R'} (hw : w ∈ Set.Icc (0 : R') 1) : + IsSubgradient V f y (w • g₁ + (1 - w) • g₂) := fun x hx ↦ by + rw [bregDiv_convexCombination] + exact add_nonneg (smul_nonneg hw.1 (h₁ x hx)) + (smul_nonneg (sub_nonneg.mpr hw.2) (h₂ x hx)) end Module @@ -191,20 +195,21 @@ variable {F_lin : Type*} [AddCommGroup F_lin] [Module R F_lin] [TopologicalSpace [LinearOrder F_lin] [IsOrderedAddMonoid F_lin] lemma IsSubgradient.max_left {f₁ f₂ : E → F_lin} {g_y : E →L[R] F_lin} - (h_sub : g_y ∈ ∂[V, y] f₁) (h_active : f₁ y = max (f₁ y) (f₂ y)) : - g_y ∈ ∂[V, y] (fun x ↦ max (f₁ x) (f₂ x)) := + (h_sub : IsSubgradient V f₁ y g_y) (h_active : f₁ y = max (f₁ y) (f₂ y)) : + IsSubgradient V (fun x ↦ max (f₁ x) (f₂ x)) y g_y := IsSubgradient.of_le_of_eq h_sub (fun x _ ↦ le_max_left (f₁ x) (f₂ x)) h_active lemma IsSubgradient.max_right {f₁ f₂ : E → F_lin} {g_y : E →L[R] F_lin} - (h_sub : g_y ∈ ∂[V, y] f₂) (h_active : f₂ y = max (f₁ y) (f₂ y)) : - g_y ∈ ∂[V, y] (fun x ↦ max (f₁ x) (f₂ x)) := + (h_sub : IsSubgradient V f₂ y g_y) (h_active : f₂ y = max (f₁ y) (f₂ y)) : + IsSubgradient V (fun x ↦ max (f₁ x) (f₂ x)) y g_y := IsSubgradient.of_le_of_eq h_sub (fun x _ ↦ le_max_right (f₁ x) (f₂ x)) h_active lemma IsSubgradient.finset_sup {ι : Type*} {s : Finset ι} {f_i : ι → E → F_lin} {i : ι} {g_y : E →L[R] F_lin} (his : i ∈ s) - (h_sub : g_y ∈ ∂[V, y] (f_i i)) (h_active : f_i i y = s.sup' ⟨i, his⟩ (fun j ↦ f_i j y)) : - g_y ∈ ∂[V, y] (fun x ↦ s.sup' ⟨i, his⟩ (fun j ↦ f_i j x)) := + (h_sub : IsSubgradient V (f_i i) y g_y) + (h_active : f_i i y = s.sup' ⟨i, his⟩ (fun j ↦ f_i j y)) : + IsSubgradient V (fun x ↦ s.sup' ⟨i, his⟩ (fun j ↦ f_i j x)) y g_y := IsSubgradient.of_le_of_eq h_sub (fun _ _ ↦ Finset.le_sup'_of_le _ his (le_refl _)) h_active end LinearOrder @@ -215,10 +220,10 @@ variable {F_lat : Type*} [AddCommGroup F_lat] [Module R F_lat] [TopologicalSpace [ConditionallyCompleteLattice F_lat] [IsOrderedAddMonoid F_lat] lemma IsSubgradient.ciSup {ι : Type*} {f_i : ι → E → F_lat} {i : ι} {g_y : E →L[R] F_lat} - (h_sub : g_y ∈ ∂[V, y] (f_i i)) + (h_sub : IsSubgradient V (f_i i) y g_y) (h_active : f_i i y = ⨆ j, f_i j y) (h_bdd : ∀ x ∈ V, BddAbove (Set.range (fun j ↦ f_i j x))) : - g_y ∈ ∂[V, y] (fun x ↦ ⨆ j, f_i j x) := + IsSubgradient V (fun x ↦ ⨆ j, f_i j x) y g_y := IsSubgradient.of_le_of_eq h_sub (fun x hx ↦ le_ciSup (h_bdd x hx) i) h_active end Lattice diff --git a/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Deriv.lean b/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Deriv.lean index bcf1671e..89abffda 100644 --- a/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Deriv.lean +++ b/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Deriv.lean @@ -13,17 +13,17 @@ public import Mathlib.Data.Set.Basic # Fréchet Derivatives and Subgradients This file establishes the connection between Fréchet derivatives (`HasFDerivAt`) -and subgradients (`∂[V, x] f`) for convex functions. +and subgradients (`IsSubgradient V f x g`) for convex functions. ## Main results -* `HasFDerivAt.mem_subdifferential`: A Fréchet derivative of a convex function +* `HasFDerivAt.isSubgradient`: A Fréchet derivative of a convex function is a subgradient. -* `HasFDerivAt.le_of_mem_subdifferential`: An interior subgradient is bounded +* `HasFDerivAt.le_of_isSubgradient`: An interior subgradient is bounded above by the Fréchet derivative. -* `HasFDerivAt.eq_of_mem_subdifferential`: Uniqueness of subgradient at interior +* `HasFDerivAt.eq_of_isSubgradient`: Uniqueness of subgradient at interior differentiable points. -* `mem_subdifferential_add_hasFDerivAt_iff`: Subdifferential sum rule when one +* `isSubgradient_add_hasFDerivAt_iff`: Subdifferential sum rule when one component is Fréchet differentiable. -/ @@ -65,24 +65,25 @@ lemma _root_.HasFDerivAt.tendsto_bregDiv_slope_zero variable [OrderClosedTopology F] /-- A Fréchet derivative of a convex function is a subgradient. -/ -lemma _root_.HasFDerivAt.mem_subdifferential +lemma _root_.HasFDerivAt.isSubgradient (hderiv : HasFDerivAt f g x) (hf : ConvexOn ℝ V f) (hx : x ∈ V) : - g ∈ ∂[V, x] f := by - refine ⟨hx, fun z hz ↦ le_of_tendsto (hderiv.tendsto_bregDiv_slope_zero (z - x)) ?_⟩ + IsSubgradient V f x g := by + intro z hz + refine le_of_tendsto (hderiv.tendsto_bregDiv_slope_zero (z - x)) ?_ 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 -lemma subgradient_of_hasFDerivAt +lemma isSubgradient_of_hasFDerivAt (hf : ConvexOn ℝ V f) (hx : x ∈ V) (hderiv : HasFDerivAt f g x) : - g ∈ ∂[V, x] f := - hderiv.mem_subdifferential hf hx + IsSubgradient V f x g := + hderiv.isSubgradient hf hx section Real variable {f : E → ℝ} {g h : E →L[ℝ] ℝ} -lemma _root_.HasFDerivAt.le_of_mem_subdifferential - (hderiv : HasFDerivAt f g x) (hV : V ∈ 𝓝 x) (hsub : h ∈ ∂[V, x] f) (w : E) : +lemma _root_.HasFDerivAt.le_of_isSubgradient + (hderiv : HasFDerivAt f g x) (hV : V ∈ 𝓝 x) (hsub : IsSubgradient V f x h) (w : E) : h w ≤ g w := by have h_nhds : (fun t : ℝ ↦ x + t • w) ⁻¹' V ∈ 𝓝 0 := (continuous_const.add (continuous_id'.smul continuous_const)).continuousAt.preimage_mem_nhds @@ -91,30 +92,30 @@ lemma _root_.HasFDerivAt.le_of_mem_subdifferential filter_upwards [nhdsWithin_le_nhds h_nhds, self_mem_nhdsWithin] with t ht_V (ht_pos : 0 < t) simpa [bregDiv, add_sub_cancel_left, h.map_smul, smul_eq_mul, inv_mul_cancel_left₀ ht_pos.ne'] using - mul_le_mul_of_nonneg_left (sub_nonneg.mp (hsub.2 (x + t • w) ht_V)) (inv_nonneg.mpr ht_pos.le) + mul_le_mul_of_nonneg_left (sub_nonneg.mp (hsub (x + t • w) ht_V)) (inv_nonneg.mpr ht_pos.le) /-- Uniqueness of the subgradient at an interior differentiable point. -/ -lemma _root_.HasFDerivAt.eq_of_mem_subdifferential - (hderiv : HasFDerivAt f g x) (hV : V ∈ 𝓝 x) (hsub : h ∈ ∂[V, x] f) : +lemma _root_.HasFDerivAt.eq_of_isSubgradient + (hderiv : HasFDerivAt f g x) (hV : V ∈ 𝓝 x) (hsub : IsSubgradient V f x h) : h = g := by ext v - exact le_antisymm (hderiv.le_of_mem_subdifferential hV hsub v) - (by simpa using hderiv.le_of_mem_subdifferential hV hsub (-v)) + exact le_antisymm (hderiv.le_of_isSubgradient hV hsub v) + (by simpa using hderiv.le_of_isSubgradient hV hsub (-v)) /-- Subdifferential sum rule when `f₁` is convex and Fréchet differentiable at `x` and `f₂` is convex on `V`: `g` is a subgradient of `f₁ + f₂` at `x` if and only if `g - g₁` is a subgradient of `f₂` at `x`. -/ -lemma _root_.HasFDerivAt.mem_subdifferential_add_iff {f₁ f₂ : E → ℝ} +lemma _root_.HasFDerivAt.isSubgradient_add_iff {f₁ f₂ : E → ℝ} {g₁ g : E →L[ℝ] ℝ} (hderiv₁ : HasFDerivAt f₁ g₁ x) (hf₁ : ConvexOn ℝ V f₁) (hf₂ : ConvexOn ℝ V f₂) (hx : x ∈ V) : - g ∈ ∂[V, x] (f₁ + f₂) ↔ (g - g₁) ∈ ∂[V, x] f₂ := by + IsSubgradient V (f₁ + f₂) x g ↔ IsSubgradient V f₂ x (g - g₁) := by have h_eq : g = g₁ + (g - g₁) := by ext; simp constructor - · rintro ⟨-, hg⟩ - refine ⟨hx, fun z hz ↦ le_of_tendsto - (by simpa using (hderiv₁.tendsto_bregDiv_slope_zero (z - x)).neg) ?_⟩ + · 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_slope : t⁻¹ • D_[f₂](x + t • (z - x), x, g - g₁) ≤ @@ -127,15 +128,15 @@ lemma _root_.HasFDerivAt.mem_subdifferential_add_iff {f₁ f₂ : E → ℝ} dsimp at * linarith · intro h₂ - have := IsSubgradient.add (hderiv₁.mem_subdifferential hf₁ hx) h₂ + have := IsSubgradient.add (hderiv₁.isSubgradient hf₁ hx) h₂ rwa [← h_eq] at this -lemma mem_subdifferential_add_hasFDerivAt_iff {f₁ f₂ : E → ℝ} +lemma isSubgradient_add_hasFDerivAt_iff {f₁ f₂ : E → ℝ} {g₁ g : E →L[ℝ] ℝ} (hf₁ : ConvexOn ℝ V f₁) (hf₂ : ConvexOn ℝ V f₂) (hx : x ∈ V) (hderiv₁ : HasFDerivAt f₁ g₁ x) : - g ∈ ∂[V, x] (f₁ + f₂) ↔ (g - g₁) ∈ ∂[V, x] f₂ := - hderiv₁.mem_subdifferential_add_iff hf₁ hf₂ hx + IsSubgradient V (f₁ + f₂) x g ↔ IsSubgradient V f₂ x (g - g₁) := + hderiv₁.isSubgradient_add_iff hf₁ hf₂ hx end Real From 73878083ea382caf7c8e7ed9a129229ee0162ff8 Mon Sep 17 00:00:00 2001 From: ISIPINK Date: Mon, 21 Sep 2026 17:46:47 +0200 Subject: [PATCH 12/15] clarified uniqueness of subgradient when fderiv --- .../ConvexAnalysis/Subgradient/Basic.lean | 4 +- .../ConvexAnalysis/Subgradient/Deriv.lean | 81 +++++++++++-------- 2 files changed, 50 insertions(+), 35 deletions(-) diff --git a/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Basic.lean b/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Basic.lean index 74db61fd..db2e9d6e 100644 --- a/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Basic.lean +++ b/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Basic.lean @@ -63,13 +63,13 @@ def subdifferential (V : Set E) (f : E → F) (y : E) : Set (E →L[R] F) := { g | IsSubgradient V f y g } /-- Scoped notation for `subdifferential`. -/ -scoped[Bregman] notation:60 "∂[" V ", " y "] " f:50 => Analysis.Convex.subdifferential V f y +scoped[Bregman] notation "∂[" V ", " y "](" f ")" => Analysis.Convex.subdifferential V f y variable {V : Set E} {f : E → F} {y x : E} {g_y : E →L[R] F} @[simp] lemma mem_subdifferential_iff : - g_y ∈ ∂[V, y] f ↔ IsSubgradient V f y g_y := Iff.rfl + g_y ∈ ∂[V, y](f) ↔ IsSubgradient V f y g_y := Iff.rfl lemma isSubgradient_const (c : F) : IsSubgradient V (fun _ ↦ c) y (0 : E →L[R] F) := by diff --git a/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Deriv.lean b/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Deriv.lean index 89abffda..91ea50a2 100644 --- a/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Deriv.lean +++ b/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Deriv.lean @@ -6,6 +6,7 @@ Authors: Isidoor Pinillo Esquivel module public import LeanMachineLearning.ForMathlib.ConvexAnalysis.Subgradient.Basic +public import Mathlib.Algebra.Group.Pointwise.Set.Basic public import Mathlib.Analysis.Calculus.LineDeriv.Basic public import Mathlib.Data.Set.Basic @@ -17,14 +18,12 @@ and subgradients (`IsSubgradient V f x g`) for convex functions. ## Main results -* `HasFDerivAt.isSubgradient`: A Fréchet derivative of a convex function - is a subgradient. -* `HasFDerivAt.le_of_isSubgradient`: An interior subgradient is bounded - above by the Fréchet derivative. -* `HasFDerivAt.eq_of_isSubgradient`: Uniqueness of subgradient at interior - differentiable points. -* `isSubgradient_add_hasFDerivAt_iff`: Subdifferential sum rule when one - component is Fréchet differentiable. +* `HasFDerivAt.isSubgradient`: A Fréchet derivative of a convex function is a subgradient. + Fréchet derivative. +* `HasFDerivAt.eq_of_isSubgradient`: Uniqueness of the subgradient at an interior differentiable + point. +* `HasFDerivAt.subdifferential_add`: Subdifferential sum rule when one component is + Fréchet differentiable. -/ @[expose] public section @@ -36,7 +35,7 @@ variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] variable [PartialOrder F] [IsOrderedAddMonoid F] [PosSMulMono ℝ F] variable {f : E → F} {V : Set E} {x : E} {g h : E →L[ℝ] F} -open scoped Bregman Topology +open scoped Bregman Topology Pointwise open Asymptotics Filter /-- Scaled Bregman divergence monotonicity along segments for convex functions. -/ @@ -73,11 +72,6 @@ lemma _root_.HasFDerivAt.isSubgradient 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 -lemma isSubgradient_of_hasFDerivAt - (hf : ConvexOn ℝ V f) (hx : x ∈ V) (hderiv : HasFDerivAt f g x) : - IsSubgradient V f x g := - hderiv.isSubgradient hf hx - section Real variable {f : E → ℝ} {g h : E →L[ℝ] ℝ} @@ -102,6 +96,22 @@ lemma _root_.HasFDerivAt.eq_of_isSubgradient exact le_antisymm (hderiv.le_of_isSubgradient hV hsub v) (by simpa using hderiv.le_of_isSubgradient hV hsub (-v)) +/-- The subdifferential of a convex, differentiable function at an interior point +is the singleton containing its derivative. -/ +lemma _root_.HasFDerivAt.subdifferential_eq + (hderiv : HasFDerivAt f g x) (hf : ConvexOn ℝ V f) (hV : V ∈ 𝓝 x) : + ∂[V, x](f) = {g} := by + ext h + simp only [mem_subdifferential_iff, Set.mem_singleton_iff] + exact ⟨fun hsub ↦ hderiv.eq_of_isSubgradient hV hsub, + fun h_eq ↦ h_eq ▸ hderiv.isSubgradient hf (mem_of_mem_nhds hV)⟩ + +/-- The subdifferential of a constant function at an interior point is `{0}` +(the normal cone to `V` at an interior point is trivial). -/ +lemma subdifferential_const_eq (c : ℝ) (hV_conv : Convex ℝ V) (hV : V ∈ 𝓝 x) : + ∂[V, x](fun _ : E ↦ c) = {(0 : E →L[ℝ] ℝ)} := + (hasFDerivAt_const c x).subdifferential_eq (convexOn_const c hV_conv) hV + /-- Subdifferential sum rule when `f₁` is convex and Fréchet differentiable at `x` and `f₂` is convex on `V`: `g` is a subgradient of `f₁ + f₂` at `x` if and only if @@ -111,32 +121,37 @@ lemma _root_.HasFDerivAt.isSubgradient_add_iff {f₁ f₂ : E → ℝ} {g₁ g : E →L[ℝ] ℝ} (hderiv₁ : HasFDerivAt f₁ g₁ x) (hf₁ : ConvexOn ℝ V f₁) (hf₂ : ConvexOn ℝ V f₂) (hx : x ∈ V) : IsSubgradient V (f₁ + f₂) x g ↔ IsSubgradient V f₂ x (g - g₁) := by - have h_eq : g = g₁ + (g - g₁) := by ext; simp 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_slope : t⁻¹ • D_[f₂](x + t • (z - x), x, g - g₁) ≤ - D_[f₂](z, x, g - g₁) := - hf₂.bregDiv_slope_le hx hz (g - g₁) ht0 ht1 + 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_slope := hf₂.bregDiv_slope_le hx hz (g - g₁) ht0 ht1 have h_nonneg := smul_nonneg (inv_nonneg.mpr ht0.le) (hg _ (hf₂.1.add_smul_sub_mem hx hz ⟨ht0.le, ht1⟩)) - have h_lin : g = g₁ + (g - g₁) := by ext; simp - rw [h_lin, bregDiv_add, smul_add] at h_nonneg + have h_eq : g = g₁ + (g - g₁) := by ext; simp + rw [h_eq, bregDiv_add, smul_add] at h_nonneg dsimp at * linarith · intro h₂ - have := IsSubgradient.add (hderiv₁.isSubgradient hf₁ hx) h₂ - rwa [← h_eq] at this - -lemma isSubgradient_add_hasFDerivAt_iff {f₁ f₂ : E → ℝ} - {g₁ g : E →L[ℝ] ℝ} - (hf₁ : ConvexOn ℝ V f₁) (hf₂ : ConvexOn ℝ V f₂) (hx : x ∈ V) - (hderiv₁ : HasFDerivAt f₁ g₁ x) : - IsSubgradient V (f₁ + f₂) x g ↔ IsSubgradient V f₂ x (g - g₁) := - hderiv₁.isSubgradient_add_iff hf₁ hf₂ hx + simpa using (hderiv₁.isSubgradient hf₁ hx).add h₂ + +/-- Subdifferential sum rule in set form: `∂[V, x](f₁ + f₂) = {g₁} + ∂[V, x](f₂)`. -/ +lemma _root_.HasFDerivAt.subdifferential_add {f₁ f₂ : E → ℝ} + {g₁ : E →L[ℝ] ℝ} (hderiv₁ : HasFDerivAt f₁ g₁ x) (hf₁ : ConvexOn ℝ V f₁) + (hf₂ : ConvexOn ℝ V f₂) (hx : x ∈ V) : + ∂[V, x](f₁ + f₂) = {g₁} + ∂[V, x](f₂) := by + ext g + simp [mem_subdifferential_iff, Set.singleton_add, hderiv₁.isSubgradient_add_iff hf₁ hf₂ hx, + add_comm g₁, sub_eq_add_neg] + +/-- When `f` is convex and Fréchet differentiable at `x ∈ V`, its subdifferential +is `g + ∂[V, x](0)` (the derivative plus the normal cone to `V` at `x`). -/ +lemma _root_.HasFDerivAt.subdifferential_eq_add_zero + (hderiv : HasFDerivAt f g x) (hf : ConvexOn ℝ V f) (hx : x ∈ V) : + ∂[V, x](f) = {g} + ∂[V, x](fun _ : E ↦ (0 : ℝ)) := by + rw [← add_zero f] + exact hderiv.subdifferential_add hf (convexOn_const (0 : ℝ) hf.1) hx end Real From c6edfc714000f15fc8252fbd1f1bc2f04b4aa468 Mon Sep 17 00:00:00 2001 From: ISIPINK Date: Mon, 21 Sep 2026 18:03:50 +0200 Subject: [PATCH 13/15] renamed to HasSubgradientWithinAt which is more accurate --- .../ConvexAnalysis/Subgradient/Basic.lean | 227 +++++++++--------- .../ConvexAnalysis/Subgradient/Deriv.lean | 101 ++++---- 2 files changed, 168 insertions(+), 160 deletions(-) diff --git a/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Basic.lean b/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Basic.lean index db2e9d6e..3173afa9 100644 --- a/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Basic.lean +++ b/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Basic.lean @@ -15,30 +15,33 @@ public import Mathlib.Tactic # Subgradients and Subdifferentials Subgradients of functions `f : E → F` defined -via the non-negativity of the Bregman divergence `0 ≤ D_[f](x, y, g_y)` on an explicit -domain `V` (i.e. the linearization error is non-negative on `V`). +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 `V : Set E` explicitly avoids using indicator functions +Carrying the domain `s : Set E` explicitly avoids using indicator functions while supporting constrained convex analysis. ## Main definitions -* `Analysis.Convex.IsSubgradient V f y g_y`: `g_y : E →L[R] F` is a subgradient of `f` - at `y` on `V`. -* `Analysis.Convex.subdifferential V f y`: The subdifferential set `∂[V, y] f`. +* `Analysis.Convex.HasSubgradientWithinAt f g s x`: `g : E →L[R] F` is a subgradient of `f` + at `x` on `s`. +* `Analysis.Convex.subdifferentialWithin f s x`: The subdifferential set `∂[s, x] (f)`. ## Main results -* Chain rules: `Analysis.Convex.IsSubgradient.comp_affine` and `Analysis.Convex.IsSubgradient.comp`. -* Equivalence with classical inequality: `Analysis.Convex.isSubgradient_iff_le`. -* Fermat's rule: `Analysis.Convex.isSubgradient_zero_iff_isMinOn`. -* Suprema and maxima: `Analysis.Convex.IsSubgradient.max_left`, - `Analysis.Convex.IsSubgradient.max_right`, `Analysis.Convex.IsSubgradient.finset_sup`, - and `Analysis.Convex.IsSubgradient.ciSup`. +* Monotonicity in the domain: `Analysis.Convex.HasSubgradientWithinAt.mono`. +* Chain rules: `Analysis.Convex.HasSubgradientWithinAt.comp_affine` and + `Analysis.Convex.HasSubgradientWithinAt.comp`. +* Equivalence with classical inequality: `Analysis.Convex.hasSubgradientWithinAt_iff_le`. +* Fermat's rule: `Analysis.Convex.hasSubgradientWithinAt_zero_iff_isMinOn`. +* Suprema and maxima: `Analysis.Convex.HasSubgradientWithinAt.max_left`, + `Analysis.Convex.HasSubgradientWithinAt.max_right`, + `Analysis.Convex.HasSubgradientWithinAt.finset_sup`, + and `Analysis.Convex.HasSubgradientWithinAt.ciSup`. ## Notation -* `∂[V, y] f`: Scoped notation in `Bregman` for `subdifferential V f y`. +* `∂[s, x] f`: Scoped notation in `Bregman` for `subdifferentialWithin f s x`. -/ @[expose] public section @@ -54,122 +57,128 @@ variable {R E E₁ F G : Type*} [Ring R] [AddCommGroup G] [Module R G] [TopologicalSpace G] [Preorder F] -/-- `g_y` is a subgradient of `f` at `y` on domain `V` (non-negativity of Bregman divergence). -/ -def IsSubgradient (V : Set E) (f : E → F) (y : E) (g_y : E →L[R] F) : Prop := - ∀ x ∈ V, 0 ≤ D_[f](x, y, g_y) +/-- `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) -/-- The subdifferential `∂[V, y] f` of `f` at `y` on `V`. -/ -def subdifferential (V : Set E) (f : E → F) (y : E) : Set (E →L[R] F) := - { g | IsSubgradient V f y g } +/-- The subdifferential `∂[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 `subdifferential`. -/ -scoped[Bregman] notation "∂[" V ", " y "](" f ")" => Analysis.Convex.subdifferential V f y +/-- Scoped notation for `subdifferentialWithin`. -/ +scoped[Bregman] notation "∂[" s ", " x "](" f ")" => Analysis.Convex.subdifferentialWithin f s x -variable {V : Set E} {f : E → F} {y x : E} {g_y : E →L[R] F} +variable {s t : Set E} {f : E → F} {x y : E} {g : E →L[R] F} @[simp] -lemma mem_subdifferential_iff : - g_y ∈ ∂[V, y](f) ↔ IsSubgradient V f y g_y := Iff.rfl +lemma mem_subdifferentialWithin : + g ∈ ∂[s, x](f) ↔ HasSubgradientWithinAt f g s x := Iff.rfl -lemma isSubgradient_const (c : F) : - IsSubgradient V (fun _ ↦ c) y (0 : E →L[R] F) := by - simp [IsSubgradient] +lemma HasSubgradientWithinAt.mono + (h : HasSubgradientWithinAt f g t x) (hst : s ⊆ t) : + HasSubgradientWithinAt f g s x := + fun y hy ↦ h y (hst hy) + +lemma hasSubgradientWithinAt_const (c : F) : + HasSubgradientWithinAt (fun _ ↦ c) (0 : E →L[R] F) s x := by + simp [HasSubgradientWithinAt] @[simp] -lemma isSubgradient_linear (h : E →L[R] F) : - IsSubgradient V h y h := by - simp [IsSubgradient] +lemma hasSubgradientWithinAt_linear (h : E →L[R] F) : + HasSubgradientWithinAt h h s x := by + simp [HasSubgradientWithinAt] @[simp] -lemma isSubgradient_add_const_iff {c : F} : - IsSubgradient V (fun x ↦ f x + c) y g_y ↔ IsSubgradient V f y g_y := by - simp [IsSubgradient, bregDiv] +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 isSubgradient_const_add_iff {c : F} : - IsSubgradient V (fun x ↦ c + f x) y g_y ↔ IsSubgradient V f y g_y := by - simp [IsSubgradient, bregDiv] +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 isSubgradient_add_linear_iff [ContinuousAdd F] {h : E →L[R] F} : - IsSubgradient V (fun x ↦ f x + h x) y (g_y + h) ↔ IsSubgradient V f y g_y := by - simp [IsSubgradient, bregDiv_add_linear] +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 isSubgradient_bregDiv_iff [IsTopologicalAddGroup F] {g_x g_y : E →L[R] F} : - IsSubgradient V (fun z ↦ D_[f](z, y, g_y)) x (g_x - g_y) ↔ IsSubgradient V f x g_x := by - simp [IsSubgradient, bregDiv_fun_bregDiv] - -lemma isSubgradient_zero_iff : - IsSubgradient V f y (0 : E →L[R] F) ↔ ∀ x ∈ V, 0 ≤ f x - f y := by - simp [IsSubgradient, bregDiv] - -lemma IsSubgradient.comp_affine - {V₁ : Set E₁} {y₁ : E₁} {A : E₁ →L[R] E} {b : E} - (h_map : ∀ x ∈ V₁, A x + b ∈ V) - (h_sub : IsSubgradient V f (A y₁ + b) g_y) : - IsSubgradient V₁ (fun x ↦ f (A x + b)) y₁ (g_y.comp A) := fun x hx ↦ by +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 x + b) (h_map x hx) + exact h_sub (A y + b) (h_map y hy) /-- **Chain rule**: `g₂ ∘ g₁` is a subgradient of `f₂ ∘ f₁` when `g₂` is non-negative. -/ -lemma IsSubgradient.comp [Preorder G] [IsOrderedAddMonoid G] +lemma HasSubgradientWithinAt.comp [Preorder G] [IsOrderedAddMonoid G] {f₂ : F → G} {f₁ : E → F} {g₂ : F →L[R] G} {g₁ : E →L[R] F} - (h₂ : IsSubgradient (f₁ '' V) f₂ (f₁ y) g₂) (h₁ : IsSubgradient V f₁ y g₁) + (h₂ : HasSubgradientWithinAt f₂ g₂ (f₁ '' s) (f₁ x)) (h₁ : HasSubgradientWithinAt f₁ g₁ s x) (hg₂_nonneg : ∀ z ≥ 0, 0 ≤ g₂ z) : - IsSubgradient V (f₂ ∘ f₁) y (g₂.comp g₁) := fun x hx ↦ by + HasSubgradientWithinAt (f₂ ∘ f₁) (g₂.comp g₁) s x := fun y hy ↦ by rw [bregDiv_comp] - exact add_nonneg (h₂ (f₁ x) ⟨x, hx, rfl⟩) (hg₂_nonneg _ (h₁ x hx)) + exact add_nonneg (h₂ (f₁ y) ⟨y, hy, rfl⟩) (hg₂_nonneg _ (h₁ y hy)) section OrderedGroup variable [IsOrderedAddMonoid F] /-- Equivalence with the classical definition. -/ -lemma isSubgradient_iff_le : - IsSubgradient V f y g_y ↔ ∀ x ∈ V, f y + g_y (x - y) ≤ f x := by - simp [IsSubgradient, bregDiv, sub_sub, sub_nonneg] +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 IsSubgradient.monotonicity [IsTopologicalAddGroup F] {g_x : E →L[R] F} - (hx : x ∈ V) (hy : y ∈ V) - (hx_sub : IsSubgradient V f x g_x) (hy_sub : IsSubgradient V f y g_y) : +lemma HasSubgradientWithinAt.monotonicity [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 isSubgradient_zero_iff_isMinOn : - IsSubgradient V f y (0 : E →L[R] F) ↔ IsMinOn f V y := by - simp [IsSubgradient, bregDiv, sub_nonneg, isMinOn_iff] +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] -lemma IsSubgradient.add [ContinuousAdd F] {f₁ f₂ : E → F} {g₁ g₂ : E →L[R] F} - (h₁ : IsSubgradient V f₁ y g₁) (h₂ : IsSubgradient V f₂ y g₂) : - IsSubgradient V (f₁ + f₂) y (g₁ + g₂) := fun x hx ↦ by +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₁ x hx) (h₂ x hx) + exact add_nonneg (h₁ y hy) (h₂ y hy) -lemma IsSubgradient.add_isMinOn [ContinuousAdd F] {f₁ f₂ : E → F} {x : E} {g : E →L[R] F} - (h_min : IsMinOn f₁ V x) (h_sub : IsSubgradient V f₂ x g) : - IsSubgradient V (f₁ + f₂) x g := by - simpa using IsSubgradient.add (isSubgradient_zero_iff_isMinOn.mpr h_min) h_sub +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 IsSubgradient.of_le_of_eq [AddRightMono F] {f₁ f₂ : E → F} {g_y : E →L[R] F} - (h_sub : IsSubgradient V f₁ y g_y) (h_le : ∀ x ∈ V, f₁ x ≤ f₂ x) (h_eq : f₁ y = f₂ y) : - IsSubgradient V f₂ y g_y := - fun x hx ↦ le_trans (h_sub x hx) - (bregDiv_le_of_le_of_eq (h_le x hx) h_eq) +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] -lemma IsSubgradient.smul {c : R'} (hc : 0 ≤ c) {f : E → F} {g_y : E →L[R'] F} - (h_sub : IsSubgradient V f y g_y) : - IsSubgradient V (c • f) y (c • g_y) := fun x hx ↦ by +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 x hx) + exact smul_nonneg hc (h_sub y hy) end ModuleBasic @@ -179,13 +188,13 @@ variable {R' : Type*} [CommRing R'] [PartialOrder R'] [IsOrderedRing R'] [Module R' E] [IsOrderedAddMonoid F] [Module R' F] [ContinuousConstSMul R' F] [PosSMulMono R' F] [ContinuousAdd F] -lemma IsSubgradient.convexCombination {f : E → F} {g₁ g₂ : E →L[R'] F} - (h₁ : IsSubgradient V f y g₁) (h₂ : IsSubgradient V f y g₂) +lemma HasSubgradientWithinAt.convexCombination {f : E → F} {g₁ g₂ : E →L[R'] F} + (h₁ : HasSubgradientWithinAt f g₁ s x) (h₂ : HasSubgradientWithinAt f g₂ s x) {w : R'} (hw : w ∈ Set.Icc (0 : R') 1) : - IsSubgradient V f y (w • g₁ + (1 - w) • g₂) := fun x hx ↦ by + HasSubgradientWithinAt f (w • g₁ + (1 - w) • g₂) s x := fun y hy ↦ by rw [bregDiv_convexCombination] - exact add_nonneg (smul_nonneg hw.1 (h₁ x hx)) - (smul_nonneg (sub_nonneg.mpr hw.2) (h₂ x hx)) + exact add_nonneg (smul_nonneg hw.1 (h₁ y hy)) + (smul_nonneg (sub_nonneg.mpr hw.2) (h₂ y hy)) end Module @@ -194,23 +203,23 @@ section LinearOrder variable {F_lin : Type*} [AddCommGroup F_lin] [Module R F_lin] [TopologicalSpace F_lin] [LinearOrder F_lin] [IsOrderedAddMonoid F_lin] -lemma IsSubgradient.max_left {f₁ f₂ : E → F_lin} {g_y : E →L[R] F_lin} - (h_sub : IsSubgradient V f₁ y g_y) (h_active : f₁ y = max (f₁ y) (f₂ y)) : - IsSubgradient V (fun x ↦ max (f₁ x) (f₂ x)) y g_y := - IsSubgradient.of_le_of_eq h_sub (fun x _ ↦ le_max_left (f₁ x) (f₂ x)) h_active +lemma HasSubgradientWithinAt.max_left {f₁ f₂ : E → F_lin} {g : E →L[R] F_lin} + (h_sub : HasSubgradientWithinAt f₁ g s x) (h_active : f₁ x = max (f₁ x) (f₂ x)) : + HasSubgradientWithinAt (fun y ↦ max (f₁ y) (f₂ y)) g s x := + h_sub.of_le_of_eq (fun y _ ↦ le_max_left (f₁ y) (f₂ y)) h_active -lemma IsSubgradient.max_right {f₁ f₂ : E → F_lin} {g_y : E →L[R] F_lin} - (h_sub : IsSubgradient V f₂ y g_y) (h_active : f₂ y = max (f₁ y) (f₂ y)) : - IsSubgradient V (fun x ↦ max (f₁ x) (f₂ x)) y g_y := - IsSubgradient.of_le_of_eq h_sub (fun x _ ↦ le_max_right (f₁ x) (f₂ x)) h_active +lemma HasSubgradientWithinAt.max_right {f₁ f₂ : E → F_lin} {g : E →L[R] F_lin} + (h_sub : HasSubgradientWithinAt f₂ g s x) (h_active : f₂ x = max (f₁ x) (f₂ x)) : + HasSubgradientWithinAt (fun y ↦ max (f₁ y) (f₂ y)) g s x := + h_sub.of_le_of_eq (fun y _ ↦ le_max_right (f₁ y) (f₂ y)) h_active -lemma IsSubgradient.finset_sup {ι : Type*} {s : Finset ι} - {f_i : ι → E → F_lin} {i : ι} {g_y : E →L[R] F_lin} - (his : i ∈ s) - (h_sub : IsSubgradient V (f_i i) y g_y) - (h_active : f_i i y = s.sup' ⟨i, his⟩ (fun j ↦ f_i j y)) : - IsSubgradient V (fun x ↦ s.sup' ⟨i, his⟩ (fun j ↦ f_i j x)) y g_y := - IsSubgradient.of_le_of_eq h_sub (fun _ _ ↦ Finset.le_sup'_of_le _ his (le_refl _)) h_active +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 : f_i i x = s_ι.sup' ⟨i, his⟩ (fun j ↦ f_i j x)) : + HasSubgradientWithinAt (fun y ↦ s_ι.sup' ⟨i, his⟩ (fun j ↦ f_i j y)) g s x := + h_sub.of_le_of_eq (fun _ _ ↦ Finset.le_sup'_of_le _ his (le_refl _)) h_active end LinearOrder @@ -219,12 +228,12 @@ section Lattice variable {F_lat : Type*} [AddCommGroup F_lat] [Module R F_lat] [TopologicalSpace F_lat] [ConditionallyCompleteLattice F_lat] [IsOrderedAddMonoid F_lat] -lemma IsSubgradient.ciSup {ι : Type*} {f_i : ι → E → F_lat} {i : ι} {g_y : E →L[R] F_lat} - (h_sub : IsSubgradient V (f_i i) y g_y) - (h_active : f_i i y = ⨆ j, f_i j y) - (h_bdd : ∀ x ∈ V, BddAbove (Set.range (fun j ↦ f_i j x))) : - IsSubgradient V (fun x ↦ ⨆ j, f_i j x) y g_y := - IsSubgradient.of_le_of_eq h_sub (fun x hx ↦ le_ciSup (h_bdd x hx) i) h_active +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 (fun j ↦ f_i j 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/ConvexAnalysis/Subgradient/Deriv.lean b/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Deriv.lean index 91ea50a2..61e7f297 100644 --- a/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Deriv.lean +++ b/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Deriv.lean @@ -14,15 +14,14 @@ public import Mathlib.Data.Set.Basic # Fréchet Derivatives and Subgradients This file establishes the connection between Fréchet derivatives (`HasFDerivAt`) -and subgradients (`IsSubgradient V f x g`) for convex functions. +and subgradients (`HasSubgradientWithinAt f g s x`) for convex functions. ## Main results -* `HasFDerivAt.isSubgradient`: A Fréchet derivative of a convex function is a subgradient. - Fréchet derivative. -* `HasFDerivAt.eq_of_isSubgradient`: Uniqueness of the subgradient at an interior differentiable - point. -* `HasFDerivAt.subdifferential_add`: Subdifferential sum rule when one component is +* `HasFDerivAt.hasSubgradientWithinAt`: A Fréchet derivative of a convex function is a subgradient. +* `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. -/ @@ -33,14 +32,14 @@ namespace Analysis.Convex variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] variable [PartialOrder F] [IsOrderedAddMonoid F] [PosSMulMono ℝ F] -variable {f : E → F} {V : Set E} {x : E} {g h : E →L[ℝ] F} +variable {f : E → F} {s : Set E} {x : E} {g h : E →L[ℝ] F} open scoped Bregman Topology Pointwise open Asymptotics Filter /-- Scaled Bregman divergence monotonicity along segments for convex functions. -/ -lemma _root_.ConvexOn.bregDiv_slope_le (hf : ConvexOn ℝ V f) - {z : E} (hx : x ∈ V) (hz : z ∈ V) (J : E →L[ℝ] F) +lemma _root_.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 @@ -64,9 +63,9 @@ lemma _root_.HasFDerivAt.tendsto_bregDiv_slope_zero variable [OrderClosedTopology F] /-- A Fréchet derivative of a convex function is a subgradient. -/ -lemma _root_.HasFDerivAt.isSubgradient - (hderiv : HasFDerivAt f g x) (hf : ConvexOn ℝ V f) (hx : x ∈ V) : - IsSubgradient V f x g := by +lemma _root_.HasFDerivAt.hasSubgradientWithinAt + (hderiv : HasFDerivAt f g x) (hf : ConvexOn ℝ s f) (hx : x ∈ s) : + HasSubgradientWithinAt f g s x := by intro z hz refine le_of_tendsto (hderiv.tendsto_bregDiv_slope_zero (z - x)) ?_ filter_upwards [self_mem_nhdsWithin, nhdsWithin_le_nhds (eventually_le_nhds zero_lt_one)] @@ -76,51 +75,51 @@ section Real variable {f : E → ℝ} {g h : E →L[ℝ] ℝ} -lemma _root_.HasFDerivAt.le_of_isSubgradient - (hderiv : HasFDerivAt f g x) (hV : V ∈ 𝓝 x) (hsub : IsSubgradient V f x h) (w : E) : +lemma _root_.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) ⁻¹' V ∈ 𝓝 0 := + 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 hV) + (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_V (ht_pos : 0 < t) + filter_upwards [nhdsWithin_le_nhds h_nhds, self_mem_nhdsWithin] with t ht_s (ht_pos : 0 < t) simpa [bregDiv, add_sub_cancel_left, h.map_smul, smul_eq_mul, inv_mul_cancel_left₀ ht_pos.ne'] using - mul_le_mul_of_nonneg_left (sub_nonneg.mp (hsub (x + t • w) ht_V)) (inv_nonneg.mpr ht_pos.le) + mul_le_mul_of_nonneg_left (sub_nonneg.mp (hsub (x + t • w) ht_s)) (inv_nonneg.mpr ht_pos.le) /-- Uniqueness of the subgradient at an interior differentiable point. -/ -lemma _root_.HasFDerivAt.eq_of_isSubgradient - (hderiv : HasFDerivAt f g x) (hV : V ∈ 𝓝 x) (hsub : IsSubgradient V f x h) : +lemma _root_.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_isSubgradient hV hsub v) - (by simpa using hderiv.le_of_isSubgradient hV hsub (-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 _root_.HasFDerivAt.subdifferential_eq - (hderiv : HasFDerivAt f g x) (hf : ConvexOn ℝ V f) (hV : V ∈ 𝓝 x) : - ∂[V, x](f) = {g} := by +lemma _root_.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_subdifferential_iff, Set.mem_singleton_iff] - exact ⟨fun hsub ↦ hderiv.eq_of_isSubgradient hV hsub, - fun h_eq ↦ h_eq ▸ hderiv.isSubgradient hf (mem_of_mem_nhds hV)⟩ + 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 `V` at an interior point is trivial). -/ -lemma subdifferential_const_eq (c : ℝ) (hV_conv : Convex ℝ V) (hV : V ∈ 𝓝 x) : - ∂[V, x](fun _ : E ↦ c) = {(0 : E →L[ℝ] ℝ)} := - (hasFDerivAt_const c x).subdifferential_eq (convexOn_const c hV_conv) hV +(the normal cone to `s` at an interior point is trivial). -/ +lemma subdifferentialWithin_const_eq (c : ℝ) (hs_conv : Convex ℝ s) (hs : s ∈ 𝓝 x) : + ∂[s, x](fun _ : E ↦ c) = {(0 : E →L[ℝ] ℝ)} := + (hasFDerivAt_const c x).subdifferentialWithin_eq (convexOn_const c hs_conv) hs /-- Subdifferential sum rule when `f₁` is convex and Fréchet differentiable at `x` -and `f₂` is convex on `V`: `g` is a subgradient of `f₁ + f₂` at `x` if and only if +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 _root_.HasFDerivAt.isSubgradient_add_iff {f₁ f₂ : E → ℝ} +lemma _root_.HasFDerivAt.hasSubgradientWithinAt_add_iff {f₁ f₂ : E → ℝ} {g₁ g : E →L[ℝ] ℝ} - (hderiv₁ : HasFDerivAt f₁ g₁ x) (hf₁ : ConvexOn ℝ V f₁) (hf₂ : ConvexOn ℝ V f₂) (hx : x ∈ V) : - IsSubgradient V (f₁ + f₂) x g ↔ IsSubgradient V f₂ x (g - g₁) := by + (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) ?_ @@ -134,24 +133,24 @@ lemma _root_.HasFDerivAt.isSubgradient_add_iff {f₁ f₂ : E → ℝ} dsimp at * linarith · intro h₂ - simpa using (hderiv₁.isSubgradient hf₁ hx).add h₂ + simpa using (hderiv₁.hasSubgradientWithinAt hf₁ hx).add h₂ -/-- Subdifferential sum rule in set form: `∂[V, x](f₁ + f₂) = {g₁} + ∂[V, x](f₂)`. -/ -lemma _root_.HasFDerivAt.subdifferential_add {f₁ f₂ : E → ℝ} - {g₁ : E →L[ℝ] ℝ} (hderiv₁ : HasFDerivAt f₁ g₁ x) (hf₁ : ConvexOn ℝ V f₁) - (hf₂ : ConvexOn ℝ V f₂) (hx : x ∈ V) : - ∂[V, x](f₁ + f₂) = {g₁} + ∂[V, x](f₂) := by +/-- Subdifferential sum rule in set form: `∂[s, x](f₁ + f₂) = {g₁} + ∂[s, x](f₂)`. -/ +lemma _root_.HasFDerivAt.subdifferentialWithin_add {f₁ f₂ : E → ℝ} + {g₁ : E →L[ℝ] ℝ} (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_subdifferential_iff, Set.singleton_add, hderiv₁.isSubgradient_add_iff hf₁ hf₂ hx, - add_comm g₁, sub_eq_add_neg] - -/-- When `f` is convex and Fréchet differentiable at `x ∈ V`, its subdifferential -is `g + ∂[V, x](0)` (the derivative plus the normal cone to `V` at `x`). -/ -lemma _root_.HasFDerivAt.subdifferential_eq_add_zero - (hderiv : HasFDerivAt f g x) (hf : ConvexOn ℝ V f) (hx : x ∈ V) : - ∂[V, x](f) = {g} + ∂[V, x](fun _ : E ↦ (0 : ℝ)) := by + 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 _root_.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 : ℝ)) := by rw [← add_zero f] - exact hderiv.subdifferential_add hf (convexOn_const (0 : ℝ) hf.1) hx + exact hderiv.subdifferentialWithin_add hf (convexOn_const (0 : ℝ) hf.1) hx end Real From f6d0e73c4ce69cfb38f0a9e5d2d2b329feb4f359 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Tue, 22 Sep 2026 09:56:55 +0200 Subject: [PATCH 14/15] improvements --- .../ConvexAnalysis/Bregman/Basic.lean | 63 ++++---- .../ConvexAnalysis/Subgradient/Basic.lean | 100 ++++++------- .../ConvexAnalysis/Subgradient/Deriv.lean | 137 ++++++++++-------- 3 files changed, 149 insertions(+), 151 deletions(-) diff --git a/LeanMachineLearning/ForMathlib/ConvexAnalysis/Bregman/Basic.lean b/LeanMachineLearning/ForMathlib/ConvexAnalysis/Bregman/Basic.lean index 11838999..f73a2349 100644 --- a/LeanMachineLearning/ForMathlib/ConvexAnalysis/Bregman/Basic.lean +++ b/LeanMachineLearning/ForMathlib/ConvexAnalysis/Bregman/Basic.lean @@ -6,8 +6,7 @@ Authors: Isidoor Pinillo Esquivel module public import Mathlib.Analysis.Convex.Function -public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic -public import Mathlib.Tactic +public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd /-! # Bregman Divergences @@ -19,9 +18,9 @@ product rules, affine invariance, and convexity preservation. ## Main definitions -* `Analysis.Convex.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). +* `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 @@ -30,8 +29,6 @@ product rules, affine invariance, and convexity preservation. @[expose] public section -namespace Analysis.Convex - variable {R E E₁ E₂ F G : Type*} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [AddCommGroup E₁] [Module R E₁] [TopologicalSpace E₁] @@ -46,7 +43,7 @@ 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 ")" => Analysis.Convex.bregDiv f x y J +scoped[Bregman] notation "D_[" f "](" x ", " y ", " J ")" => bregDiv f x y J open scoped Bregman @@ -70,6 +67,7 @@ lemma bregDiv_fun_bregDiv [IsTopologicalAddGroup F] : 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] @@ -108,7 +106,7 @@ lemma bregDiv_add_linear [ContinuousAdd F] (h : E →L[R] F) : simp only [bregDiv, add_apply, map_sub] abel -@[simp] +@[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] @@ -118,7 +116,7 @@ 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_translate (x₀ : E) : +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] @@ -139,10 +137,11 @@ end ChainRules section CommRing -variable {R' : Type*} [CommRing R'] [TopologicalSpace R'] [IsTopologicalAddGroup R'] - [ContinuousSMul R' R'] [Module R' E] +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₂) + @@ -167,48 +166,36 @@ end Order section Module -variable {R' : Type*} [CommRing R'] [Module R' E] [Module R' F] - [ContinuousAdd F] [ContinuousConstSMul R' F] +variable {R' : Type*} [CommRing R'] [Module R' E] [Module R' F] [ContinuousConstSMul R' F] -omit [ContinuousAdd F] in 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 (f : E → F) (x y : E) (J₁ J₂ : E →L[R'] F) (w : R') : - D_[f](x, y, w • J₁ + (1 - w) • J₂) = w • D_[f](x, y, J₁) + (1 - w) • D_[f](x, y, J₂) := by - calc - D_[f](x, y, w • J₁ + (1 - w) • J₂) - = D_[(w + (1 - w)) • f](x, y, w • J₁ + (1 - w) • J₂) := by - rw [add_sub_cancel, one_smul] - _ = D_[w • f](x, y, w • J₁) + D_[(1 - w) • f](x, y, (1 - w) • J₂) := by - rw [add_smul, bregDiv_add] - _ = w • D_[f](x, y, J₁) + (1 - w) • D_[f](x, y, J₂) := by - simp only [bregDiv_smul] +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 {𝕜 E' F' : Type*} [Ring 𝕜] [PartialOrder 𝕜] -variable [AddCommGroup E'] [Module 𝕜 E'] [TopologicalSpace E'] -variable [AddCommGroup F'] [Module 𝕜 F'] [TopologicalSpace F'] - [PartialOrder F'] [IsOrderedAddMonoid F'] +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`. -/ -lemma _root_.ConvexOn.bregDiv {s : Set E'} {f : E' → F'} (hf : ConvexOn 𝕜 s f) - (J : E' →L[𝕜] F') (y : E') : - ConvexOn 𝕜 s (fun x ↦ D_[f](x, y, J)) := by - simp only [Analysis.Convex.bregDiv, sub_eq_add_neg, map_add, map_neg, neg_add_rev, neg_neg] +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 ConvexOn.add - · exact hf - · exact convexOn_const (-f y) hf.1 + · 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 - -end Analysis.Convex diff --git a/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Basic.lean b/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Basic.lean index 3173afa9..2544e19e 100644 --- a/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Basic.lean +++ b/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Basic.lean @@ -6,10 +6,6 @@ Authors: Isidoor Pinillo Esquivel module public import LeanMachineLearning.ForMathlib.ConvexAnalysis.Bregman.Basic -public import Mathlib.Analysis.Convex.Function -public import Mathlib.Order.ConditionallyCompleteLattice.Basic -public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic -public import Mathlib.Tactic /-! # Subgradients and Subdifferentials @@ -23,31 +19,25 @@ while supporting constrained convex analysis. ## Main definitions -* `Analysis.Convex.HasSubgradientWithinAt f g s x`: `g : E →L[R] F` is a subgradient of `f` - at `x` on `s`. -* `Analysis.Convex.subdifferentialWithin f s x`: The subdifferential set `∂[s, x] (f)`. +* `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: `Analysis.Convex.HasSubgradientWithinAt.mono`. -* Chain rules: `Analysis.Convex.HasSubgradientWithinAt.comp_affine` and - `Analysis.Convex.HasSubgradientWithinAt.comp`. -* Equivalence with classical inequality: `Analysis.Convex.hasSubgradientWithinAt_iff_le`. -* Fermat's rule: `Analysis.Convex.hasSubgradientWithinAt_zero_iff_isMinOn`. -* Suprema and maxima: `Analysis.Convex.HasSubgradientWithinAt.max_left`, - `Analysis.Convex.HasSubgradientWithinAt.max_right`, - `Analysis.Convex.HasSubgradientWithinAt.finset_sup`, - and `Analysis.Convex.HasSubgradientWithinAt.ciSup`. +* 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 -* `∂[s, x] f`: Scoped notation in `Bregman` for `subdifferentialWithin f s x`. +* `∂[R, s, x](f)`: Scoped notation in `Bregman` for `subdifferentialWithin R f s x`. -/ @[expose] public section -namespace Analysis.Convex - open scoped Bregman variable {R E E₁ F G : Type*} [Ring R] @@ -61,24 +51,26 @@ variable {R E E₁ F G : Type*} [Ring R] def HasSubgradientWithinAt (f : E → F) (g : E →L[R] F) (s : Set E) (x : E) : Prop := ∀ y ∈ s, 0 ≤ D_[f](y, x, g) -/-- The subdifferential `∂[s, x] f` of `f` at `x` on `s`. -/ +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 "∂[" s ", " x "](" f ")" => Analysis.Convex.subdifferentialWithin f s x +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 ∈ ∂[s, x](f) ↔ HasSubgradientWithinAt f g s x := Iff.rfl + 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] @@ -121,14 +113,14 @@ lemma HasSubgradientWithinAt.comp_affine 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 non-negative. -/ +/-- **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₂_nonneg : ∀ z ≥ 0, 0 ≤ g₂ z) : + (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⟩) (hg₂_nonneg _ (h₁ y hy)) + exact add_nonneg (h₂ (f₁ y) ⟨y, hy, rfl⟩) (by grw [← hg₂ (h₁ y hy)]; simp) section OrderedGroup @@ -139,7 +131,7 @@ 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.monotonicity [IsTopologicalAddGroup F] {g_x g_y : E →L[R] F} +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 @@ -150,12 +142,14 @@ 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 @@ -174,6 +168,7 @@ 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 @@ -184,44 +179,51 @@ end ModuleBasic section Module -variable {R' : Type*} [CommRing R'] [PartialOrder R'] [IsOrderedRing R'] +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) - {w : R'} (hw : w ∈ Set.Icc (0 : R') 1) : - HasSubgradientWithinAt f (w • g₁ + (1 - w) • g₂) s x := fun y hy ↦ by - rw [bregDiv_convexCombination] - exact add_nonneg (smul_nonneg hw.1 (h₁ y hy)) - (smul_nonneg (sub_nonneg.mpr hw.2) (h₂ y hy)) + {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 LinearOrder +section SemilatticeSup variable {F_lin : Type*} [AddCommGroup F_lin] [Module R F_lin] [TopologicalSpace F_lin] - [LinearOrder F_lin] [IsOrderedAddMonoid F_lin] + [SemilatticeSup F_lin] [IsOrderedAddMonoid F_lin] -lemma HasSubgradientWithinAt.max_left {f₁ f₂ : E → F_lin} {g : E →L[R] F_lin} - (h_sub : HasSubgradientWithinAt f₁ g s x) (h_active : f₁ x = max (f₁ x) (f₂ x)) : - HasSubgradientWithinAt (fun y ↦ max (f₁ y) (f₂ y)) g s x := - h_sub.of_le_of_eq (fun y _ ↦ le_max_left (f₁ y) (f₂ y)) h_active +@[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) -lemma HasSubgradientWithinAt.max_right {f₁ f₂ : E → F_lin} {g : E →L[R] F_lin} - (h_sub : HasSubgradientWithinAt f₂ g s x) (h_active : f₂ x = max (f₁ x) (f₂ x)) : - HasSubgradientWithinAt (fun y ↦ max (f₁ y) (f₂ y)) g s x := - h_sub.of_le_of_eq (fun y _ ↦ le_max_right (f₁ y) (f₂ y)) h_active +@[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 ι} +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 : f_i i x = s_ι.sup' ⟨i, his⟩ (fun j ↦ f_i j x)) : - HasSubgradientWithinAt (fun y ↦ s_ι.sup' ⟨i, his⟩ (fun j ↦ f_i j y)) g s x := - h_sub.of_le_of_eq (fun _ _ ↦ Finset.le_sup'_of_le _ his (le_refl _)) h_active + (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 LinearOrder +end SemilatticeSup section Lattice @@ -231,10 +233,8 @@ variable {F_lat : Type*} [AddCommGroup F_lat] [Module R F_lat] [TopologicalSpace 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 (fun j ↦ f_i j y))) : + (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 - -end Analysis.Convex diff --git a/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Deriv.lean b/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Deriv.lean index 61e7f297..935ea44a 100644 --- a/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Deriv.lean +++ b/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Deriv.lean @@ -6,19 +6,19 @@ Authors: Isidoor Pinillo Esquivel module public import LeanMachineLearning.ForMathlib.ConvexAnalysis.Subgradient.Basic -public import Mathlib.Algebra.Group.Pointwise.Set.Basic public import Mathlib.Analysis.Calculus.LineDeriv.Basic -public import Mathlib.Data.Set.Basic /-! # Fréchet Derivatives and Subgradients -This file establishes the connection between Fréchet derivatives (`HasFDerivAt`) -and subgradients (`HasSubgradientWithinAt f g s x`) for convex functions. +This file establishes the connection between Fréchet derivatives (`HasFDerivWithinAt`, +`HasFDerivAt`) and subgradients (`HasSubgradientWithinAt f g s x`) for convex functions. ## Main results -* `HasFDerivAt.hasSubgradientWithinAt`: A Fréchet derivative of a convex function is a subgradient. +* `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 @@ -27,31 +27,29 @@ and subgradients (`HasSubgradientWithinAt f g s x`) for convex functions. @[expose] public section -namespace Analysis.Convex - variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] -variable [PartialOrder F] [IsOrderedAddMonoid F] [PosSMulMono ℝ F] variable {f : E → F} {s : Set E} {x : E} {g h : E →L[ℝ] F} open scoped Bregman Topology Pointwise -open Asymptotics Filter - -/-- Scaled Bregman divergence monotonicity along segments for convex functions. -/ -lemma _root_.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) +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] -omit [PartialOrder F] [IsOrderedAddMonoid F] [PosSMulMono ℝ F] in /-- As the step size `t → 0⁺`, the linearization error of a Fréchet differentiable function scaled by `t⁻¹` converges to `0`. -/ -lemma _root_.HasFDerivAt.tendsto_bregDiv_slope_zero +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) @@ -60,22 +58,42 @@ lemma _root_.HasFDerivAt.tendsto_bregDiv_slope_zero 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 of a convex function is a subgradient. -/ -lemma _root_.HasFDerivAt.hasSubgradientWithinAt - (hderiv : HasFDerivAt f g x) (hf : ConvexOn ℝ s f) (hx : x ∈ s) : +/-- 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 - refine le_of_tendsto (hderiv.tendsto_bregDiv_slope_zero (z - x)) ?_ + 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 -section Real - -variable {f : E → ℝ} {g h : E →L[ℝ] ℝ} +/-- 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 _root_.HasFDerivAt.le_of_hasSubgradientWithinAt +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 := @@ -83,12 +101,13 @@ lemma _root_.HasFDerivAt.le_of_hasSubgradientWithinAt (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) - simpa [bregDiv, add_sub_cancel_left, h.map_smul, smul_eq_mul, - inv_mul_cancel_left₀ ht_pos.ne'] using - mul_le_mul_of_nonneg_left (sub_nonneg.mp (hsub (x + t • w) ht_s)) (inv_nonneg.mpr ht_pos.le) + 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 _root_.HasFDerivAt.eq_of_hasSubgradientWithinAt +lemma HasFDerivAt.eq_of_hasSubgradientWithinAt (hderiv : HasFDerivAt f g x) (hs : s ∈ 𝓝 x) (hsub : HasSubgradientWithinAt f h s x) : h = g := by ext v @@ -97,9 +116,9 @@ lemma _root_.HasFDerivAt.eq_of_hasSubgradientWithinAt /-- The subdifferential of a convex, differentiable function at an interior point is the singleton containing its derivative. -/ -lemma _root_.HasFDerivAt.subdifferentialWithin_eq +lemma HasFDerivAt.subdifferentialWithin_eq (hderiv : HasFDerivAt f g x) (hf : ConvexOn ℝ s f) (hs : s ∈ 𝓝 x) : - ∂[s, x](f) = {g} := by + ∂[ℝ, s, x](f) = {g} := by ext h simp only [mem_subdifferentialWithin, Set.mem_singleton_iff] exact ⟨fun hsub ↦ hderiv.eq_of_hasSubgradientWithinAt hs hsub, @@ -107,17 +126,17 @@ lemma _root_.HasFDerivAt.subdifferentialWithin_eq /-- 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 : ℝ) (hs_conv : Convex ℝ s) (hs : s ∈ 𝓝 x) : - ∂[s, x](fun _ : E ↦ c) = {(0 : E →L[ℝ] ℝ)} := - (hasFDerivAt_const c x).subdifferentialWithin_eq (convexOn_const c hs_conv) hs +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` +/-- 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 _root_.HasFDerivAt.hasSubgradientWithinAt_add_iff {f₁ f₂ : E → ℝ} - {g₁ g : E →L[ℝ] ℝ} +`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 @@ -125,33 +144,25 @@ lemma _root_.HasFDerivAt.hasSubgradientWithinAt_add_iff {f₁ f₂ : E → ℝ} 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_slope := hf₂.bregDiv_slope_le hx hz (g - g₁) ht0 ht1 have h_nonneg := smul_nonneg (inv_nonneg.mpr ht0.le) (hg _ (hf₂.1.add_smul_sub_mem hx hz ⟨ht0.le, ht1⟩)) - have h_eq : g = g₁ + (g - g₁) := by ext; simp - rw [h_eq, bregDiv_add, smul_add] at h_nonneg - dsimp at * - linarith + 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 _root_.HasFDerivAt.subdifferentialWithin_add {f₁ f₂ : E → ℝ} - {g₁ : E →L[ℝ] ℝ} (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 +/-- 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 _root_.HasFDerivAt.subdifferentialWithin_eq_add_zero +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 : ℝ)) := by + ∂[ℝ, s, x](f) = {g} + ∂[ℝ, s, x](fun _ : E ↦ (0 : F)) := by rw [← add_zero f] - exact hderiv.subdifferentialWithin_add hf (convexOn_const (0 : ℝ) hf.1) hx - -end Real - -end Analysis.Convex + exact hderiv.subdifferentialWithin_add hf (convexOn_const (0 : F) hf.1) hx From f9400ffdf8d782ebf6bbfe6919804a1a4d86de6a Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Tue, 22 Sep 2026 09:58:27 +0200 Subject: [PATCH 15/15] move files --- LeanMachineLearning.lean | 6 +++--- .../{ConvexAnalysis => Analysis/Convex}/Bregman/Basic.lean | 0 .../Convex}/Subgradient/Basic.lean | 2 +- .../Convex}/Subgradient/Deriv.lean | 2 +- 4 files changed, 5 insertions(+), 5 deletions(-) rename LeanMachineLearning/ForMathlib/{ConvexAnalysis => Analysis/Convex}/Bregman/Basic.lean (100%) rename LeanMachineLearning/ForMathlib/{ConvexAnalysis => Analysis/Convex}/Subgradient/Basic.lean (99%) rename LeanMachineLearning/ForMathlib/{ConvexAnalysis => Analysis/Convex}/Subgradient/Deriv.lean (99%) diff --git a/LeanMachineLearning.lean b/LeanMachineLearning.lean index eeaeecb3..ef058a9c 100644 --- a/LeanMachineLearning.lean +++ b/LeanMachineLearning.lean @@ -1,8 +1,8 @@ module -- shake: keep-all --deprecated_module: ignore -public import LeanMachineLearning.ForMathlib.ConvexAnalysis.Bregman.Basic -public import LeanMachineLearning.ForMathlib.ConvexAnalysis.Subgradient.Basic -public import LeanMachineLearning.ForMathlib.ConvexAnalysis.Subgradient.Deriv +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/ConvexAnalysis/Bregman/Basic.lean b/LeanMachineLearning/ForMathlib/Analysis/Convex/Bregman/Basic.lean similarity index 100% rename from LeanMachineLearning/ForMathlib/ConvexAnalysis/Bregman/Basic.lean rename to LeanMachineLearning/ForMathlib/Analysis/Convex/Bregman/Basic.lean diff --git a/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Basic.lean b/LeanMachineLearning/ForMathlib/Analysis/Convex/Subgradient/Basic.lean similarity index 99% rename from LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Basic.lean rename to LeanMachineLearning/ForMathlib/Analysis/Convex/Subgradient/Basic.lean index 2544e19e..578da360 100644 --- a/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Basic.lean +++ b/LeanMachineLearning/ForMathlib/Analysis/Convex/Subgradient/Basic.lean @@ -5,7 +5,7 @@ Authors: Isidoor Pinillo Esquivel -/ module -public import LeanMachineLearning.ForMathlib.ConvexAnalysis.Bregman.Basic +public import LeanMachineLearning.ForMathlib.Analysis.Convex.Bregman.Basic /-! # Subgradients and Subdifferentials diff --git a/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Deriv.lean b/LeanMachineLearning/ForMathlib/Analysis/Convex/Subgradient/Deriv.lean similarity index 99% rename from LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Deriv.lean rename to LeanMachineLearning/ForMathlib/Analysis/Convex/Subgradient/Deriv.lean index 935ea44a..8510abad 100644 --- a/LeanMachineLearning/ForMathlib/ConvexAnalysis/Subgradient/Deriv.lean +++ b/LeanMachineLearning/ForMathlib/Analysis/Convex/Subgradient/Deriv.lean @@ -5,7 +5,7 @@ Authors: Isidoor Pinillo Esquivel -/ module -public import LeanMachineLearning.ForMathlib.ConvexAnalysis.Subgradient.Basic +public import LeanMachineLearning.ForMathlib.Analysis.Convex.Subgradient.Basic public import Mathlib.Analysis.Calculus.LineDeriv.Basic /-!