Subgradients and Subdifferentials

Subgradients of functions f : E → F defined via the non-negativity of the Bregman divergence 0 ≤ D_[f](y, x, g) on an explicit domain s (i.e. the linearization error is non-negative on s).

Carrying the domain s : Set E explicitly avoids using indicator functions while supporting constrained convex analysis.

Main definitions

• HasSubgradientWithinAt f g s x: g : E →L[R] F is a subgradient of f at x on s.
• subdifferentialWithin R f s x: The subdifferential set ∂[R, s, x](f).

Main results

• Monotonicity in the domain: HasSubgradientWithinAt.mono.
• Chain rules: HasSubgradientWithinAt.comp_affine and HasSubgradientWithinAt.comp.
• Equivalence with classical inequality: hasSubgradientWithinAt_iff_le.
• Fermat's rule: hasSubgradientWithinAt_zero_iff_isMinOn.
• Suprema and maxima: HasSubgradientWithinAt.sup_left, HasSubgradientWithinAt.sup_right, HasSubgradientWithinAt.finset_sup', and HasSubgradientWithinAt.ciSup.

Notation

• ∂[R, s, x](f): Scoped notation in Bregman for subdifferentialWithin R f s x.

def HasSubgradientWithinAt {R : Type u_1} {E : Type u_2} {F : Type u_4} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [AddCommGroup F] [Module R F] [TopologicalSpace F] [Preorder F] (f : E → F) (g : E →L[R] F) (s : Set E) (x : E) : Prop

g is a subgradient of f at x on domain s (non-negativity of Bregman divergence).

Equations

• HasSubgradientWithinAt f g s x = ∀ y ∈ s, 0 ≤ bregDiv f y x g

def subdifferentialWithin (R : Type u_1) {E : Type u_2} {F : Type u_4} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [AddCommGroup F] [Module R F] [TopologicalSpace F] [Preorder F] (f : E → F) (s : Set E) (x : E) : Set (E →L[R] F)

The subdifferential ∂[R, s, x](f) of f at x on s.

Equations

• subdifferentialWithin R f s x = {g : E →L[R] F | HasSubgradientWithinAt f g s x}

def Bregman.«term∂[_,_,_](_)» : Lean.ParserDescr

Scoped notation for subdifferentialWithin.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem mem_subdifferentialWithin {R : Type u_1} {E : Type u_2} {F : Type u_4} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [AddCommGroup F] [Module R F] [TopologicalSpace F] [Preorder F] {s : Set E} {f : E → F} {x : E} {g : E →L[R] F} : g ∈ subdifferentialWithin R f s x ↔ HasSubgradientWithinAt f g s x

theorem HasSubgradientWithinAt.mono {R : Type u_1} {E : Type u_2} {F : Type u_4} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [AddCommGroup F] [Module R F] [TopologicalSpace F] [Preorder F] {s t : Set E} {f : E → F} {x : E} {g : E →L[R] F} (h : HasSubgradientWithinAt f g t x) (hst : s ⊆ t) : HasSubgradientWithinAt f g s x

@[simp]

theorem hasSubgradientWithinAt_const {R : Type u_1} {E : Type u_2} {F : Type u_4} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [AddCommGroup F] [Module R F] [TopologicalSpace F] [Preorder F] {s : Set E} {x : E} (c : F) : HasSubgradientWithinAt (fun (x : E) => c) 0 s x

@[simp]

theorem hasSubgradientWithinAt_linear {R : Type u_1} {E : Type u_2} {F : Type u_4} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [AddCommGroup F] [Module R F] [TopologicalSpace F] [Preorder F] {s : Set E} {x : E} (h : E →L[R] F) : HasSubgradientWithinAt (⇑h) h s x

@[simp]

theorem hasSubgradientWithinAt_add_const_iff {R : Type u_1} {E : Type u_2} {F : Type u_4} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [AddCommGroup F] [Module R F] [TopologicalSpace F] [Preorder F] {s : Set E} {f : E → F} {x : E} {g : E →L[R] F} {c : F} : HasSubgradientWithinAt (fun (y : E) => f y + c) g s x ↔ HasSubgradientWithinAt f g s x

@[simp]

theorem hasSubgradientWithinAt_const_add_iff {R : Type u_1} {E : Type u_2} {F : Type u_4} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [AddCommGroup F] [Module R F] [TopologicalSpace F] [Preorder F] {s : Set E} {f : E → F} {x : E} {g : E →L[R] F} {c : F} : HasSubgradientWithinAt (fun (y : E) => c + f y) g s x ↔ HasSubgradientWithinAt f g s x

@[simp]

theorem hasSubgradientWithinAt_add_linear_iff {R : Type u_1} {E : Type u_2} {F : Type u_4} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [AddCommGroup F] [Module R F] [TopologicalSpace F] [Preorder F] {s : Set E} {f : E → F} {x : E} {g : E →L[R] F} [ContinuousAdd F] {h : E →L[R] F} : HasSubgradientWithinAt (fun (y : E) => f y + h y) (g + h) s x ↔ HasSubgradientWithinAt f g s x

@[simp]

theorem hasSubgradientWithinAt_bregDiv_iff {R : Type u_1} {E : Type u_2} {F : Type u_4} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [AddCommGroup F] [Module R F] [TopologicalSpace F] [Preorder F] {s : Set E} {f : E → F} {x y : E} [IsTopologicalAddGroup F] {g_x g_y : E →L[R] F} : HasSubgradientWithinAt (fun (z : E) => bregDiv f z y g_y) (g_x - g_y) s x ↔ HasSubgradientWithinAt f g_x s x

theorem hasSubgradientWithinAt_zero_iff {R : Type u_1} {E : Type u_2} {F : Type u_4} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [AddCommGroup F] [Module R F] [TopologicalSpace F] [Preorder F] {s : Set E} {f : E → F} {x : E} : HasSubgradientWithinAt f 0 s x ↔ ∀ y ∈ s, 0 ≤ f y - f x

theorem HasSubgradientWithinAt.comp_affine {R : Type u_1} {E : Type u_2} {E₁ : Type u_3} {F : Type u_4} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [AddCommGroup E₁] [Module R E₁] [TopologicalSpace E₁] [AddCommGroup F] [Module R F] [TopologicalSpace F] [Preorder F] {s : Set E} {f : E → F} {g : E →L[R] F} {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 : E₁) => f (A y + b)) (g ∘SL A) s₁ x₁

theorem HasSubgradientWithinAt.comp {R : Type u_1} {E : Type u_2} {F : Type u_4} {G : Type u_5} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [AddCommGroup F] [Module R F] [TopologicalSpace F] [AddCommGroup G] [Module R G] [TopologicalSpace G] [Preorder F] {s : Set E} {x : E} [Preorder G] [IsOrderedAddMonoid G] {f₂ : F → G} {f₁ : E → F} {g₂ : F →L[R] G} {g₁ : E →L[R] F} (h₂ : HasSubgradientWithinAt f₂ g₂ (f₁ '' s) (f₁ x)) (h₁ : HasSubgradientWithinAt f₁ g₁ s x) (hg₂ : Monotone ⇑g₂) : HasSubgradientWithinAt (f₂ ∘ f₁) (g₂ ∘SL g₁) s x

Chain rule: g₂ ∘ g₁ is a subgradient of f₂ ∘ f₁ when g₂ is monotone.

theorem hasSubgradientWithinAt_iff_le {R : Type u_1} {E : Type u_2} {F : Type u_4} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [AddCommGroup F] [Module R F] [TopologicalSpace F] [Preorder F] {s : Set E} {f : E → F} {x : E} {g : E →L[R] F} [IsOrderedAddMonoid F] : HasSubgradientWithinAt f g s x ↔ ∀ y ∈ s, f x + g (y - x) ≤ f y

Equivalence with the classical definition.

theorem HasSubgradientWithinAt.sub_apply_sub_nonneg {R : Type u_1} {E : Type u_2} {F : Type u_4} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [AddCommGroup F] [Module R F] [TopologicalSpace F] [Preorder F] {s : Set E} {f : E → F} {x y : E} [IsOrderedAddMonoid F] [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)

theorem hasSubgradientWithinAt_zero_iff_isMinOn {R : Type u_1} {E : Type u_2} {F : Type u_4} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [AddCommGroup F] [Module R F] [TopologicalSpace F] [Preorder F] {s : Set E} {f : E → F} {x : E} [IsOrderedAddMonoid F] : HasSubgradientWithinAt f 0 s x ↔ IsMinOn f s x

theorem HasSubgradientWithinAt.add {R : Type u_1} {E : Type u_2} {F : Type u_4} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [AddCommGroup F] [Module R F] [TopologicalSpace F] [Preorder F] {s : Set E} {x : E} [IsOrderedAddMonoid F] [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

theorem HasSubgradientWithinAt.fun_add {R : Type u_1} {E : Type u_2} {F : Type u_4} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [AddCommGroup F] [Module R F] [TopologicalSpace F] [Preorder F] {s : Set E} {x : E} [IsOrderedAddMonoid F] [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 (fun (i : E) => f₁ i + f₂ i) (g₁ + g₂) s x

Eta-expanded form of HasSubgradientWithinAt.add

theorem HasSubgradientWithinAt.add_isMinOn {R : Type u_1} {E : Type u_2} {F : Type u_4} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [AddCommGroup F] [Module R F] [TopologicalSpace F] [Preorder F] {s : Set E} [IsOrderedAddMonoid F] [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

theorem HasSubgradientWithinAt.fun_add_isMinOn {R : Type u_1} {E : Type u_2} {F : Type u_4} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [AddCommGroup F] [Module R F] [TopologicalSpace F] [Preorder F] {s : Set E} [IsOrderedAddMonoid F] [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 (fun (i : E) => f₁ i + f₂ i) g s x

Eta-expanded form of HasSubgradientWithinAt.add_isMinOn

theorem HasSubgradientWithinAt.of_le_of_eq {R : Type u_1} {E : Type u_2} {F : Type u_4} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] [AddCommGroup F] [Module R F] [TopologicalSpace F] [Preorder F] {s : Set E} {x : E} [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

theorem HasSubgradientWithinAt.smul {E : Type u_2} {F : Type u_4} [AddCommGroup E] [TopologicalSpace E] [AddCommGroup F] [TopologicalSpace F] [Preorder F] {s : Set E} {x : E} {R' : Type u_6} [CommRing R'] [PartialOrder R'] [Module R' E] [Module R' F] [ContinuousConstSMul R' F] [PosSMulMono R' F] {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

theorem HasSubgradientWithinAt.fun_smul {E : Type u_2} {F : Type u_4} [AddCommGroup E] [TopologicalSpace E] [AddCommGroup F] [TopologicalSpace F] [Preorder F] {s : Set E} {x : E} {R' : Type u_6} [CommRing R'] [PartialOrder R'] [Module R' E] [Module R' F] [ContinuousConstSMul R' F] [PosSMulMono R' F] {c : R'} (hc : 0 ≤ c) {f : E → F} {g : E →L[R'] F} (h_sub : HasSubgradientWithinAt f g s x) : HasSubgradientWithinAt (fun (i : E) => c • f i) (c • g) s x

Eta-expanded form of HasSubgradientWithinAt.smul

theorem HasSubgradientWithinAt.convexCombination {E : Type u_2} {F : Type u_4} [AddCommGroup E] [TopologicalSpace E] [AddCommGroup F] [TopologicalSpace F] [Preorder F] {s : Set E} {x : E} {R' : Type u_6} [CommRing R'] [PartialOrder R'] [Module R' E] [IsOrderedAddMonoid F] [Module R' F] [ContinuousConstSMul R' F] [PosSMulMono R' F] [ContinuousAdd F] {f : E → F} {g₁ g₂ : E →L[R'] F} (h₁ : HasSubgradientWithinAt f g₁ s x) (h₂ : HasSubgradientWithinAt f g₂ s x) {a b : R'} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) : HasSubgradientWithinAt f (a • g₁ + b • g₂) s x

theorem convex_subdifferentialWithin {E : Type u_2} {F : Type u_4} [AddCommGroup E] [TopologicalSpace E] [AddCommGroup F] [TopologicalSpace F] [Preorder F] {s : Set E} {f : E → F} {x : E} {R' : Type u_6} [CommRing R'] [PartialOrder R'] [Module R' E] [IsOrderedAddMonoid F] [Module R' F] [ContinuousConstSMul R' F] [PosSMulMono R' F] [ContinuousAdd F] : Convex R' (subdifferentialWithin R' f s x)

theorem HasSubgradientWithinAt.sup_left {R : Type u_1} {E : Type u_2} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] {s : Set E} {x : E} {F_lin : Type u_6} [AddCommGroup F_lin] [Module R F_lin] [TopologicalSpace F_lin] [SemilatticeSup F_lin] [IsOrderedAddMonoid F_lin] {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

theorem HasSubgradientWithinAt.fun_sup_left {R : Type u_1} {E : Type u_2} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] {s : Set E} {x : E} {F_lin : Type u_6} [AddCommGroup F_lin] [Module R F_lin] [TopologicalSpace F_lin] [SemilatticeSup F_lin] [IsOrderedAddMonoid F_lin] {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 (fun (i : E) => f₁ i ⊔ f₂ i) g s x

Eta-expanded form of HasSubgradientWithinAt.sup_left

theorem HasSubgradientWithinAt.sup_right {R : Type u_1} {E : Type u_2} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] {s : Set E} {x : E} {F_lin : Type u_6} [AddCommGroup F_lin] [Module R F_lin] [TopologicalSpace F_lin] [SemilatticeSup F_lin] [IsOrderedAddMonoid F_lin] {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

theorem HasSubgradientWithinAt.fun_sup_right {R : Type u_1} {E : Type u_2} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] {s : Set E} {x : E} {F_lin : Type u_6} [AddCommGroup F_lin] [Module R F_lin] [TopologicalSpace F_lin] [SemilatticeSup F_lin] [IsOrderedAddMonoid F_lin] {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 (fun (i : E) => f₁ i ⊔ f₂ i) g s x

Eta-expanded form of HasSubgradientWithinAt.sup_right

theorem HasSubgradientWithinAt.finset_sup' {R : Type u_1} {E : Type u_2} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] {s : Set E} {x : E} {F_lin : Type u_6} [AddCommGroup F_lin] [Module R F_lin] [TopologicalSpace F_lin] [SemilatticeSup F_lin] [IsOrderedAddMonoid F_lin] {ι : Type u_7} {s_ι : Finset ι} {f_i : ι → E → F_lin} {i : ι} {g : E →L[R] F_lin} (his : i ∈ s_ι) (h_sub : HasSubgradientWithinAt (f_i i) g s x) (h_active : ∀ j ∈ s_ι, f_i j x ≤ f_i i x) : HasSubgradientWithinAt (fun (y : E) => s_ι.sup' ⋯ fun (x : ι) => f_i x y) g s x

theorem HasSubgradientWithinAt.ciSup {R : Type u_1} {E : Type u_2} [Ring R] [AddCommGroup E] [Module R E] [TopologicalSpace E] {s : Set E} {x : E} {F_lat : Type u_6} [AddCommGroup F_lat] [Module R F_lat] [TopologicalSpace F_lat] [ConditionallyCompleteLattice F_lat] [IsOrderedAddMonoid F_lat] {ι : Type u_7} {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 (x : ι) => f_i x y)) : HasSubgradientWithinAt (fun (y : E) => ⨆ (j : ι), f_i j y) g s x