Documentation

Mathlib.Analysis.NormedSpace.HahnBanach.Extension

Extension Hahn-Banach theorem #

In this file we prove the analytic Hahn-Banach theorem. For any continuous linear function on a subspace, we can extend it to a function on the entire space without changing its norm.

We prove

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 Real.exists_extension_norm_eq {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace 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 . See also exists_extension_norm_eq in the root namespace for a more general version that works both for and .

theorem exists_extension_norm_eq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 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 𝕜 satisfying IsRCLikeNormedField 𝕜.

theorem ContinuousLinearMap.exist_extension_of_finiteDimensional_range {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] {E : Type u_2} {F : Type u_3} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : Submodule 𝕜 E} (f : p →L[𝕜] F) [FiniteDimensional 𝕜 (LinearMap.range f)] :
∃ (g : E →L[𝕜] F), f = g.comp p.subtypeL

Corollary of the Hahn-Banach theorem: if f : p → F is a continuous linear map from a submodule of a normed space E over 𝕜, 𝕜 = ℝ or 𝕜 = ℂ, with a finite dimensional range, then f admits an extension to a continuous linear map E → F.

Note that contrary to the case F = 𝕜, see exists_extension_norm_eq, we provide no estimates on the norm of the extension.

theorem Submodule.ClosedComplemented.of_finiteDimensional {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : Submodule 𝕜 F) [FiniteDimensional 𝕜 p] :
p.ClosedComplemented

A finite dimensional submodule over or is Submodule.ClosedComplemented.

theorem coord_norm' (𝕜 : Type v) [RCLike 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} (h : x 0) :
theorem exists_dual_vector (𝕜 : Type v) [RCLike 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 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) [RCLike 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 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) [RCLike 𝕜] {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 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).