mathlib documentation

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

@[class]
structure has_exists_extension_norm_eq (𝕜 : Type v) [nondiscrete_normed_field 𝕜] :
Prop

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 .

Instances
def norm' (𝕜 : Type u_1) [nondiscrete_normed_field 𝕜] [normed_algebra 𝕜] {E : Type u_2} [normed_group E] :
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
theorem norm'_def (𝕜 : Type u_1) [nondiscrete_normed_field 𝕜] [normed_algebra 𝕜] {E : Type u_2} [normed_group E] (x : E) :

theorem norm_norm' (𝕜 : Type u_1) [nondiscrete_normed_field 𝕜] [normed_algebra 𝕜] (A : Type u_2) [normed_group A] (x : A) :

theorem exists_extension_norm_eq {E : Type u_1} [normed_group E] [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 .

Restrict a -subspace to an -subspace.

Equations
theorem complex.exists_extension_norm_eq {F : Type u_1} [normed_group F] [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 .

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

theorem exists_dual_vector {𝕜 : Type v} [nondiscrete_normed_field 𝕜] [normed_algebra 𝕜] {E : Type u} [normed_group E] [normed_space 𝕜 E] [has_exists_extension_norm_eq 𝕜] (x : E) :
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∥.

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

Variant of the above theorem, eliminating the hypothesis that x be nonzero, and choosing the dual element arbitrarily when x = 0.