noncomputable def support_function {E : Type u} [AddCommGroup E] [Module ℝ E] (C : Set E) : Module.Dual ℝ E → EReal

Definition 2.9: the support function of a set C ⊆ E is the extended-real-valued function on the dual space E* = Module.Dual ℝ E sending y to the supremum of the pairings y x for x ∈ C. For nonempty C, this realizes the textbook codomain (-∞, ∞].

def termσ__ : Lean.ParserDescr

Textbook notation for the dual-space support function σ_C.

@[simp]

theorem support_function_apply {E : Type u} [AddCommGroup E] [Module ℝ E] (C : Set E) (y : Module.Dual ℝ E) : (σ_ C) y = sSup ((fun (x : E) => ↑(y x)) '' C)

Evaluating the support function at y gives the supremum of the dual pairings y x over x ∈ C.

theorem le_support_function_of_mem {E : Type u} [AddCommGroup E] [Module ℝ E] {C : Set E} {x : E} (hx : x ∈ C) (y : Module.Dual ℝ E) : ↑(y x) ≤ (σ_ C) y

Every point of C gives a lower bound on the support function of C.

theorem bot_lt_support_function {E : Type u} [AddCommGroup E] [Module ℝ E] (C : Set E) (hC : C.Nonempty) (y : Module.Dual ℝ E) : ⊥ < (σ_ C) y

For a nonempty set C, the support function is strictly above -∞.

theorem support_function_ne_bot {E : Type u} [AddCommGroup E] [Module ℝ E] (C : Set E) (hC : C.Nonempty) (y : Module.Dual ℝ E) : (σ_ C) y ≠ ⊥

For a nonempty set C, the support function never takes the value -∞.

theorem support_function_eq_of_isGreatest_image {E : Type u} [AddCommGroup E] [Module ℝ E] (C : Set E) (y : Module.Dual ℝ E) {a : EReal} (hmax : IsGreatest ((fun (x : E) => ↑(y x)) '' C) a) : (σ_ C) y = a

If the pairing image y '' C has greatest element a, then the support function of C at y is exactly a.