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 introduce a typeclass
has_exists_extension_norm_eq for a field, requiring that a strong version of the
Hahn-Banach theorem holds over this field, and provide instances for ℝ and ℂ.
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 𝕜).
- exists_extension_norm_eq : ∀ (E : Type ?) [_inst_1_1 : normed_group E] [_inst_2 : normed_space 𝕜 E] (p : subspace 𝕜 E) (f : ↥p →L[𝕜] 𝕜), ∃ (g : E →L[𝕜] 𝕜), (∀ (x : ↥p), ⇑g ↑x = ⇑f x) ∧ ∥g∥ = ∥f∥
A field where the Hahn-Banach theorem for continuous linear functions holds. This allows stating theorems that depend on it uniformly over such fields.
In particular, this is satisfied by ℝ and ℂ.
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
Restrict a ℂ-subspace to an ℝ-subspace.
Equations
Equations
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∥.
Variant of the above theorem, eliminating the hypothesis that x be nonzero, and choosing
the dual element arbitrarily when x = 0.