Hahn-Banach theorem for polynormable spaces

In this file, we prove the analytic Hahn-Banach theorem for polynormable spaces over a field satisfying IsRCLikeNormedField. For any continuous linear functional on a subspace, we can extend it to the entire space. Note that we cannot use LocallyConvexSpace because an IsRCLikeNormedField has no order structure.

We prove

• Module.Dual.exists_continuous_extension_of_le_seminorm: Hahn-Banach theorem for linear functionals dominated by a continuous seminorm on polynormable spaces over a field satisfying IsRCLikeNormedField.
• StrongDual.exists_extension: Hahn-Banach theorem for continuous linear functionals on polynormable spaces over fields satisfying IsRCLikeNormedField.

theorem Module.Dual.exists_extension_of_le_seminorm_real {E : Type u_2} [AddCommGroup E] [Module ℝ E] (S : Subspace ℝ E) (f : Dual ℝ ↥S) {p : Seminorm ℝ E} (hp : ∀ (x : ↥S), f x ≤ p ↑x) : ∃ (g : Dual ℝ E), (∀ (x : ↥S), g ↑x = f x) ∧ ∀ (x : E), |g x| ≤ p x

theorem Module.Dual.exists_extension_of_le_seminorm {𝕜 : Type u_1} {E : Type u_2} [AddCommGroup E] [NormedField 𝕜] [IsRCLikeNormedField 𝕜] [Module 𝕜 E] (S : Submodule 𝕜 E) (f : Dual 𝕜 ↥S) {p : Seminorm 𝕜 E} (hp : ∀ (x : ↥S), ‖f x‖ ≤ p ↑x) : ∃ (g : Dual 𝕜 E), (∀ (x : ↥S), g ↑x = f x) ∧ ∀ (x : E), ‖g x‖ ≤ p x

theorem Module.Dual.exists_continuous_extension_of_le_seminorm_real {E : Type u_2} [AddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] [Module ℝ E] [ContinuousSMul ℝ E] [PolynormableSpace ℝ E] (S : Subspace ℝ E) (f : Dual ℝ ↥S) {p : Seminorm ℝ E} (hp_cont : Continuous ⇑p) (hp : ∀ (x : ↥S), f x ≤ p ↑x) : ∃ (g : StrongDual ℝ E), (∀ (x : ↥S), g ↑x = f x) ∧ ∀ (x : E), |g x| ≤ p x

Hahn-Banach theorem for linear functionals dominated by a continuous seminorm on polynormable spaces over ℝ.

theorem Module.Dual.exists_continuous_extension_of_le_seminorm {𝕜 : Type u_1} {E : Type u_2} [AddCommGroup E] [NormedField 𝕜] [IsRCLikeNormedField 𝕜] [TopologicalSpace E] [Module 𝕜 E] [PolynormableSpace 𝕜 E] (S : Submodule 𝕜 E) (f : Dual 𝕜 ↥S) {p : Seminorm 𝕜 E} (hp_cont : Continuous ⇑p) (hp : ∀ (x : ↥S), ‖f x‖ ≤ p ↑x) : ∃ (g : StrongDual 𝕜 E), (∀ (x : ↥S), g ↑x = f x) ∧ ∀ (x : E), ‖g x‖ ≤ p x

Hahn-Banach theorem for linear functionals dominated by a continuous seminorm on polynormable spaces over fields satisfying IsRCLikeNormedField.

theorem StrongDual.exists_extension {E : Type u_2} [AddCommGroup E] [TopologicalSpace E] {𝕜 : Type u_3} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [Module 𝕜 E] [PolynormableSpace 𝕜 E] (S : Submodule 𝕜 E) (f : StrongDual 𝕜 ↥S) : ∃ (g : StrongDual 𝕜 E), ∀ (x : ↥S), g ↑x = f x

Hahn-Banach theorem for continuous linear functionals on polynormable spaces over a field satisfying IsRCLikeNormedField.

theorem ContinuousLinearMap.exist_extension_of_finiteDimensional_range {𝕜 : Type u_1} {E : Type u_2} [AddCommGroup E] [NormedField 𝕜] [IsRCLikeNormedField 𝕜] [TopologicalSpace E] [Module 𝕜 E] [PolynormableSpace 𝕜 E] {F : Type u_3} [AddCommGroup F] [TopologicalSpace F] [IsTopologicalAddGroup F] [Module 𝕜 F] [ContinuousSMul 𝕜 F] [T2Space F] {S : Submodule 𝕜 E} (f : ↥S →L[𝕜] F) [FiniteDimensional 𝕜 ↥(↑f).range] : ∃ (g : E →L[𝕜] F), f = g ∘SL S.subtypeL

Corollary of the polynormable Hahn-Banach theorem: if f : S → F is a continuous linear map with finite-dimensional range, then f extends to a continuous linear map on the whole space.

theorem Submodule.ClosedComplemented.of_finiteDimensional {𝕜 : Type u_1} [NormedField 𝕜] [IsRCLikeNormedField 𝕜] {F : Type u_3} [AddCommGroup F] [TopologicalSpace F] [IsTopologicalAddGroup F] [Module 𝕜 F] [ContinuousSMul 𝕜 F] [T2Space F] [PolynormableSpace 𝕜 F] (S : Submodule 𝕜 F) [FiniteDimensional 𝕜 ↥S] : S.ClosedComplemented

A finite-dimensional submodule of a polynormable space over a field satisfying IsRCLikeNormedField is Submodule.ClosedComplemented.