Documentation

Convex.Function.Subgradient

Subgradient of convex functions #

The file defines subgradient for convex functions in E and proves some basic properties.

Let f : E → ℝ be a convex function on s and g : E, where s is a set of E. g is a subgradient of f at x if for any y ∈ s, we have f y ≥ f x + inner g (y - x). The insight comes from the first order condition of convex function.

Main declarations #

HasSubgradientAt f g x: The function f has subgradient g at x.
HasSubgradientWithinAt f g s x: The function f has subgradient g at x within s.
SubderivAt f x: The subderiv of f at x is the collection of all possible subgradients of f at x.
SubderivWithinAt f s x: The subderiv of f at x within s is the collection of all possible subgradients of f at x within s.

Main results #

SubderivWithinAt_eq_gradient: The subderiv of differentiable convex functions is the singleton of its gradient.
HasSubgradientAt_zero_iff_isMinOn: 0 is a subgradient of f at x if and only if x is a minimizer of f.

def HasSubgradientAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (f : E → ℝ) (g : E) (x : E) :

Subgradient of functions -

Equations

HasSubgradientAt f g x = ∀ (y : E), f y ≥ f x + ⟪g, y - x⟫_ℝ

Instances For

def HasSubgradientWithinAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (f : E → ℝ) (g : E) (s : Set E) (x : E) :

Equations

HasSubgradientWithinAt f g s x = ∀ y ∈ s, f y ≥ f x + ⟪g, y - x⟫_ℝ

Instances For

def SubderivAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (f : E → ℝ) (x : E) :

Subderiv of functions -

Equations

SubderivAt f x = {g : E | HasSubgradientAt f g x}

Instances For

def SubderivWithinAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (f : E → ℝ) (s : Set E) (x : E) :

Equations

SubderivWithinAt f s x = {g : E | HasSubgradientWithinAt f g s x}

Instances For

@[simp]

theorem mem_SubderivAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : E → ℝ} {g : E} {x : E} :

HasSubgradientAt f g x ↔ g ∈ SubderivAt f x

@[simp]

theorem hasSubgradientWithinAt_univ {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : E → ℝ} {g : E} {x : E} :

HasSubgradientWithinAt f g Set.univ x ↔ HasSubgradientAt f g x

theorem HasSubgradientAt.hasSubgradientWithinAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : E → ℝ} {g : E} {x : E} {s : Set E} :

HasSubgradientAt f g x → HasSubgradientWithinAt f g s x

theorem SubderivAt_SubderivWithinAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : E → ℝ} {x : E} :

SubderivAt f x = SubderivWithinAt f Set.univ x

theorem HasSubgradientAt_HasBanachSubgradientAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {g : E} {x : E} :

HasSubgradientAt f g x ↔ Banach_HasSubgradientAt f ((InnerProductSpace.toDual ℝ E) g) x

theorem HasBanachSubgradientAt_HasSubgradientAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {g : E →L[ℝ ] ℝ} {x : E} :

Banach_HasSubgradientAt f g x ↔ HasSubgradientAt f ((InnerProductSpace.toDual ℝ E).symm g) x

theorem HasSubgradientWithinAt_HasBanachSubgradientWithinAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {s : Set E} {f : E → ℝ} {g : E} {x : E} :

HasSubgradientWithinAt f g s x ↔ Banach_HasSubgradientWithinAt f ((InnerProductSpace.toDual ℝ E) g) s x

theorem HasBanachSubgradientWithinAt_HasSubgradientWithinAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {s : Set E} {f : E → ℝ} {g : E →L[ℝ ] ℝ} {x : E} :

Banach_HasSubgradientWithinAt f g s x ↔ HasSubgradientWithinAt f ((InnerProductSpace.toDual ℝ E).symm g) s x

Congruence properties of the `Subderiv` #

theorem SubderivAt.congr {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {x : E} {f₁ : E → ℝ} {f₂ : E → ℝ} (h : f₁ = f₂) :

SubderivAt f₁ x = SubderivAt f₂ x

theorem SubderivWithinAt.congr {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {x : E} {f₁ : E → ℝ} {f₂ : E → ℝ} {s : Set E} (h : ∀ y ∈ s, f₁ y = f₂ y) (hf : f₁ x = f₂ x) :

SubderivWithinAt f₁ s x = SubderivWithinAt f₂ s x

theorem SubderivWithinAt.congr_of_mem {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {x : E} {f₁ : E → ℝ} {f₂ : E → ℝ} {s : Set E} (xs : x ∈ s) (h : ∀ y ∈ s, f₁ y = f₂ y) :

SubderivWithinAt f₁ s x = SubderivWithinAt f₂ s x

theorem SubderivAt.congr_mono {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {x : E} {f₁ : E → ℝ} {f₂ : E → ℝ} {t : Set E} {s : Set E} (h : ∀ y ∈ s, f₁ y = f₂ y) (hx : f₁ x = f₂ x) (h₁ : t ⊆ s) :

SubderivWithinAt f₁ t x = SubderivWithinAt f₂ t x

Basic properties about `Subderiv` #

theorem SubderivWithinAt.Nonempty {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {s : Set E} (hf : ConvexOn ℝ s f) (hc : ContinuousOn f (interior s)) (x : E) :

x ∈ interior s → (SubderivWithinAt f s x).Nonempty

theorem SubderivAt.nonempty {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} (hf : ConvexOn ℝ Set.univ f) (hc : ContinuousOn f Set.univ) (x : E) :

Nonempty ↑(SubderivAt f x)

theorem SubderivAt.isClosed {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : E → ℝ} (x : E) :

IsClosed (SubderivAt f x)

The subderiv of f at x is a closed set. -

theorem SubderivWithinAt.isClosed {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : E → ℝ} {s : Set E} (x : E) :

IsClosed (SubderivWithinAt f s x)

theorem SubderivAt.convex {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : E → ℝ} (x : E) :

Convex ℝ (SubderivAt f x)

The subderiv of f at x is a convex set. -

theorem SubderivWithinAt.convex {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : E → ℝ} {s : Set E} (x : E) :

x ∈ s → Convex ℝ (SubderivWithinAt f s x)

theorem subgradientAt_mono {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {x : E} {y : E} {u : E} {v : E} {f : E → ℝ} (hu : u ∈ SubderivAt f x) (hv : v ∈ SubderivAt f y) :

⟪u - v, x - y⟫_ℝ ≥ 0

Monotonicity of subderiv-

Calculation of `Subderiv` #

theorem SubderivWithinAt_eq_gradient {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {x : E} {s : Set E} {f'x : E} (hx : x ∈ interior s) (hf : ConvexOn ℝ s f) (h : HasGradientAt f f'x x) :

SubderivWithinAt f s x = {f'x}

Subderiv of differentiable convex functions -

theorem SubderivWithinAt_eq_FDeriv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {x : E} {s : Set E} {f' : E → E →L[ℝ ] ℝ} (hx : x ∈ interior s) (hf : ConvexOn ℝ s f) (h : HasFDerivAt f (f' x) x) :

SubderivWithinAt f s x = {(InnerProductSpace.toDual ℝ E).symm (f' x)}

Alternarive version for FDeriv -

theorem SubderivAt_eq_gradient {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f : E → ℝ} {x : E} {f'x : E} (hf : ConvexOn ℝ Set.univ f) (h : HasGradientAt f f'x x) :

SubderivAt f x = {f'x}

Optimality Theory for Unconstrained Nondifferentiable Problems #

theorem HasSubgradientAt_zero_of_isMinOn {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : E → ℝ} {x : E} (h : IsMinOn f Set.univ x) :

HasSubgradientAt f 0 x

theorem isMinOn_of_HasSubgradentAt_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : E → ℝ} {x : E} (h : HasSubgradientAt f 0 x) :

IsMinOn f Set.univ x

theorem HasSubgradientAt_zero_iff_isMinOn {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : E → ℝ} {x : E} :

HasSubgradientAt f 0 x ↔ IsMinOn f Set.univ x

x' minimize f if and only if 0 is a subgradient of f at x' -

theorem HasSubgradientWithinAt_zero_of_isMinOn {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : E → ℝ} {x : E} {s : Set E} (h : IsMinOn f s x) :

HasSubgradientWithinAt f 0 s x

theorem isMinOn_of_HasSubgradentWithinAt_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : E → ℝ} {x : E} {s : Set E} (h : HasSubgradientWithinAt f 0 s x) :

theorem HasSubgradientWithinAt_zero_iff_isMinOn {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : E → ℝ} {x : E} {s : Set E} :

HasSubgradientWithinAt f 0 s x ↔ IsMinOn f s x

Computing `Subderiv` #

theorem HasSubgradientAt.pos_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : E → ℝ} {g : E} {x : E} {c : ℝ} (h : HasSubgradientAt f g x) (hc : 0 < c) :

HasSubgradientAt (c • f) (c • g) x

Multiplication by a Positive Scalar-

theorem SubderivAt.pos_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f : E → ℝ} {x : E} {c : ℝ} (hc : 0 < c) :

SubderivAt (c • f) x = c • SubderivAt f x

theorem SubderivAt.add_subset {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {f₁ : E → ℝ} {f₂ : E → ℝ} (x : E) :

SubderivAt f₁ x + SubderivAt f₂ x ⊆ SubderivAt (f₁ + f₂) x

Subderivatives of the sum of two functions is a subset of the sum of the subderivatives of the two functions -

theorem SubderivAt.add {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {f₁ : E → ℝ} {f₂ : E → ℝ} (h₁ : ConvexOn ℝ Set.univ f₁) (h₂ : ConvexOn ℝ Set.univ f₂) (hcon : ContinuousOn f₁ Set.univ) (x : E) :

SubderivAt f₁ x + SubderivAt f₂ x = SubderivAt (f₁ + f₂) x

Examples of `Subderiv` #

theorem SubderivAt_of_norm_at_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] :

SubderivAt (fun (x : E) => ‖x‖) 0 = {g : E | ‖g‖ ≤ 1}

theorem SubderivAt_abs (x : ℝ) :

SubderivAt abs x = if x = 0 then Set.Icc (-1) 1 else {x.sign}