# mathlibdocumentation

analysis.normed_space.hahn_banach

# 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 𝕜).

theorem real.exists_extension_norm_eq {E : Type u_1} [ E] (p : E) (f : p →L[] ) :
∃ (g : E →L[] ), (∀ (x : p), g x = f x) g = f

Hahn-Banach theorem for continuous linear functions over ℝ.

theorem exists_extension_norm_eq {𝕜 : Type u_1} [is_R_or_C 𝕜] {F : Type u_2} [ F] (p : 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 𝕜.

theorem coord_norm' (𝕜 : Type v) [is_R_or_C 𝕜] {E : Type u} [normed_group E] [ E] {x : E} (h : x 0) :
theorem exists_dual_vector (𝕜 : Type v) [is_R_or_C 𝕜] {E : Type u} [normed_group E] [ E] (x : E) (h : x 0) :
∃ (g : E →L[𝕜] 𝕜), g = 1 g x = 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∥.

theorem exists_dual_vector' (𝕜 : Type v) [is_R_or_C 𝕜] {E : Type u} [normed_group E] [ E] [nontrivial E] (x : E) :
∃ (g : E →L[𝕜] 𝕜), g = 1 g x = x

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

theorem exists_dual_vector'' (𝕜 : Type v) [is_R_or_C 𝕜] {E : Type u} [normed_group E] [ E] (x : E) :
∃ (g : E →L[𝕜] 𝕜), g 1 g x = x

Variant of Hahn-Banach, eliminating the hypothesis that x be nonzero, but only ensuring that the dual element has norm at most 1 (this can not be improved for the trivial vector space).