Hahn-Banach extension theorem

In this file, we prove the analytic Hahn-Banach theorem for normed vector spaces. For any continuous linear functional on a subspace, we can extend it to the entire space without changing its norm. For Hahn-Banach theorems for locally convex spaces, see Mathlib.Analysis.LocallyConvex.HahnBanach.

We prove

• exists_extension_norm_eq: Hahn-Banach theorem for continuous linear functionals on normed spaces over ℝ or ℂ.

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

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 exists_extension_norm_eq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (p : Subspace 𝕜 E) (f : StrongDual 𝕜 ↥p) : ∃ (g : StrongDual 𝕜 E), (∀ (x : ↥p), g ↑x = f x) ∧ ‖g‖ = ‖f‖

Hahn-Banach theorem for continuous linear functions over 𝕜 satisfying IsRCLikeNormedField 𝕜.

theorem exists_dual_vector (𝕜 : Type v) [RCLike 𝕜] {E : Type u} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (x : E) (h : ‖x‖ ≠ 0) : ∃ (g : StrongDual 𝕜 E), ‖g‖ = 1 ∧ g x = ↑‖x‖

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

theorem exists_dual_vector'' (𝕜 : Type v) [RCLike 𝕜] {E : Type u} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (x : E) : ∃ (g : StrongDual 𝕜 E), ‖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 cannot be improved for the trivial vector space).

theorem exists_dual_vector' (𝕜 : Type v) [RCLike 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [Nontrivial E] (x : E) : ∃ (g : StrongDual 𝕜 E), ‖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.