def Banach_HasSubgradientAt {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (f : E → ℝ) (g : E →L[ℝ] ℝ) (x : E) : Prop

Subgradient of functions -

Equations

• Banach_HasSubgradientAt f g x = ∀ (y : E), f y ≥ f x + g (y - x)

def Banach_HasSubgradientWithinAt {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (f : E → ℝ) (g : E →L[ℝ] ℝ) (s : Set E) (x : E) : Prop

Equations

• Banach_HasSubgradientWithinAt f g s x = ∀ y ∈ s, f y ≥ f x + g (y - x)

def Banach_SubderivAt {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (f : E → ℝ) (x : E) : Set (E →L[ℝ] ℝ)

Subderiv of functions -

Equations

• Banach_SubderivAt f x = {g : E →L[ℝ] ℝ | Banach_HasSubgradientAt f g x}

def Banach_SubderivWithinAt {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] (f : E → ℝ) (s : Set E) (x : E) : Set (E →L[ℝ] ℝ)

Equations

• Banach_SubderivWithinAt f s x = {g : E →L[ℝ] ℝ | Banach_HasSubgradientWithinAt f g s x}

def Epi {E : Type u_1} (f : E → ℝ) (s : Set E) : Set (E × ℝ)

Equations

• Epi f s = {p : E × ℝ | p.1 ∈ s ∧ f p.1 ≤ p.2}

theorem EpigraphInterior_existence {E : Type u_1} [SeminormedAddCommGroup E] {f : E → ℝ} {x : E} {s : Set E} (hc : ContinuousOn f (interior s)) (hx : x ∈ interior s) (t : ℝ) : t > f x → (x, t) ∈ interior {p : E × ℝ | p.1 ∈ s ∧ f p.1 ≤ p.2}

theorem mem_epi_frontier {E : Type u_1} [SeminormedAddCommGroup E] {f : E → ℝ} {s : Set E} (y : E) : y ∈ interior s → (y, f y) ∈ frontier {p : E × ℝ | p.1 ∈ s ∧ f p.1 ≤ p.2}

theorem Banach_SubderivWithinAt.Nonempty {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {f : E → ℝ} {x : E} {s : Set E} (hf : ConvexOn ℝ s f) (hc : ContinuousOn f (interior s)) (hx : x ∈ interior s) : (Banach_SubderivWithinAt f s x).Nonempty