Hahn-Banach theorem #

In this file we prove a version of Hahn-Banach theorem for continuous linear functions on normed spaces over ℝ and ℂ.

In order to state and prove its corollaries uniformly, we prove the statements for a field 𝕜 satisfying is_R_or_C 𝕜.

In this setting, exists_dual_vector states that, for any nonzero x, there exists a continuous linear form g of norm 1 with g x = ∥x∥ (where the norm has to be interpreted as an element of 𝕜).

source

def norm' (𝕜 : Type u_1) [nondiscrete_normed_field 𝕜] [semi_normed_algebra ℝ 𝕜] {E : Type u_2} [semi_normed_group E] (x : E) :

𝕜

The norm of x as an element of 𝕜 (a normed algebra over ℝ). This is needed in particular to state equalities of the form g x = norm' 𝕜 x when g is a linear function.

For the concrete cases of ℝ and ℂ, this is just ∥x∥ and ↑∥x∥, respectively.

Equations

norm' 𝕜 x = ⇑(algebra_map ℝ 𝕜) ∥x∥

source

theorem norm'_def (𝕜 : Type u_1) [nondiscrete_normed_field 𝕜] [semi_normed_algebra ℝ 𝕜] {E : Type u_2} [semi_normed_group E] (x : E) :

norm' 𝕜 x = ⇑(algebra_map ℝ 𝕜) ∥x∥

source

theorem norm_norm' (𝕜 : Type u_1) [nondiscrete_normed_field 𝕜] [semi_normed_algebra ℝ 𝕜] (A : Type u_2) [semi_normed_group A] (x : A) :

∥norm' 𝕜 x∥ = ∥x∥

source

theorem real.exists_extension_norm_eq {E : Type u_1} [semi_normed_group E] [semi_normed_space ℝ E] (p : subspace ℝ E) (f : ↥p →L[ℝ ] ℝ) :

∃ (g : E →L[ℝ ] ℝ), (∀ (x : ↥p), ⇑g ↑x = ⇑f x) ∧ ∥g∥ = ∥f∥

Hahn-Banach theorem for continuous linear functions over ℝ.

source

theorem exists_extension_norm_eq {𝕜 : Type u_1} [is_R_or_C 𝕜] {F : Type u_2} [semi_normed_group F] [semi_normed_space 𝕜 F] (p : subspace 𝕜 F) (f : ↥p →L[𝕜] 𝕜) :

∃ (g : F →L[𝕜] 𝕜), (∀ (x : ↥p), ⇑g ↑x = ⇑f x) ∧ ∥g∥ = ∥f∥

Hahn-Banach theorem for continuous linear functions over 𝕜 satisyfing is_R_or_C 𝕜.

source

theorem coord_norm' {𝕜 : Type v} [is_R_or_C 𝕜] {E : Type u} [normed_group E] [normed_space 𝕜 E] (x : E) (h : x ≠ 0) :

∥norm' 𝕜 x • continuous_linear_equiv.coord 𝕜 x h∥ = 1

source

theorem exists_dual_vector {𝕜 : Type v} [is_R_or_C 𝕜] {E : Type u} [normed_group E] [normed_space 𝕜 E] (x : E) (h : x ≠ 0) :

∃ (g : E →L[𝕜] 𝕜), ∥g∥ = 1 ∧ ⇑g x = norm' 𝕜 x

Corollary of Hahn-Banach. Given a nonzero element x of a normed space, there exists an element of the dual space, of norm 1, whose value on x is ∥x∥.

source

theorem exists_dual_vector' {𝕜 : Type v} [is_R_or_C 𝕜] {E : Type u} [normed_group E] [normed_space 𝕜 E] [nontrivial E] (x : E) :

∃ (g : E →L[𝕜] 𝕜), ∥g∥ = 1 ∧ ⇑g x = norm' 𝕜 x

Variant of Hahn-Banach, eliminating the hypothesis that x be nonzero, and choosing the dual element arbitrarily when x = 0.