Mathlib/Analysis/LocallyConvex/HahnBanach.lean

Exact source: Mathlib/Analysis/LocallyConvex/HahnBanach.lean

Pinned GitHub source · Raw UTF-8 source

Back to Each satellite norms its coefficient preimage in absolute value

1/-2Copyright (c) 2026 Yongxi Lin. All rights reserved.3Released under Apache 2.0 license as described in the file LICENSE.4Authors: Yongxi Lin5-/6module78public import Mathlib.Analysis.Convex.Cone.Extension9public import Mathlib.Analysis.LocallyConvex.AbsConvexOpen10public import Mathlib.Analysis.LocallyConvex.WeakDual11public import Mathlib.Analysis.Normed.Module.RCLike.Extend12public import Mathlib.Topology.Algebra.Module.FiniteDimension1314/-!15# Hahn-Banach theorem for polynormable spaces1617In this file, we prove the analytic Hahn-Banach theorem for polynormable spaces over a field18satisfying `IsRCLikeNormedField`. For any continuous linear functional on a subspace, we can extend19it to the entire space. Note that we cannot use `LocallyConvexSpace` because an20`IsRCLikeNormedField` has no order structure.2122We prove23* `Module.Dual.exists_continuous_extension_of_le_seminorm`: Hahn-Banach theorem for linear24  functionals dominated by a continuous seminorm on polynormable spaces over a field satisfying25  `IsRCLikeNormedField`.26* `StrongDual.exists_extension`: Hahn-Banach theorem for continuous linear functionals on27  polynormable spaces over fields satisfying `IsRCLikeNormedField`.2829-/3031public section3233open Module Topology RCLike3435open scoped ComplexConjugate3637variable {𝕜 E : Type*} [AddCommGroup E]3839theorem Module.Dual.exists_extension_of_le_seminorm_real [Module ℝ E]40    (S : Subspace ℝ E) (f : Dual ℝ S)41    {p : Seminorm ℝ E} (hp : ∀ x, f x ≤ p x) :42    ∃ g : Dual ℝ E, (∀ x : S, g x = f x) ∧ ∀ x, |g x| ≤ p x := by43  obtain ⟨g, hg, hl⟩ := by44    refine exists_extension_of_le_sublinear ⟨S, f⟩ p (fun _ hc _ => ?_) ?_ hp45    · simp [map_smul_eq_mul, abs_of_nonneg hc.le]46    · exact fun x y => map_add_le_add p x y47  exact ⟨g, hg, p.abs_le_of_le hl⟩4849variable [NormedField 𝕜] [IsRCLikeNormedField 𝕜]5051theorem Module.Dual.exists_extension_of_le_seminorm [Module 𝕜 E] (S : Submodule 𝕜 E) (f : Dual 𝕜 S)52    {p : Seminorm 𝕜 E} (hp : ∀ x, ‖f x‖ ≤ p x) :53    ∃ g : Dual 𝕜 E, (∀ x : S, g x = f x) ∧ ∀ x, ‖g x‖ ≤ p x := by54  letI : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜55  letI : Module ℝ E := .restrictScalars ℝ 𝕜 E56  letI : IsScalarTower ℝ 𝕜 E := .restrictScalars _ _ _57  let fr : Dual ℝ S := reLm.comp (f.restrictScalars ℝ)58  obtain ⟨g, (hg : ∀ x : S, g x = fr x), hgp⟩ :=59    fr.exists_extension_of_le_seminorm_real (S.restrictScalars ℝ) (p := p.restrictScalars ℝ)60      fun x ↦ (re_le_norm (f x)).trans (hp x)61  refine ⟨g.extendRCLike, fun x ↦ ?_, fun x ↦ ?_⟩62  · rw [g.extendRCLike_apply, ← Submodule.coe_smul, hg, hg]63    simp [fr, mul_comm I]64  · apply norm_extendRCLike_le_seminorm65    exact hgp6667variable [TopologicalSpace E]6869/-- **Hahn-Banach theorem** for linear functionals dominated by a continuous seminorm on70polynormable spaces over `ℝ`. -/71theorem Module.Dual.exists_continuous_extension_of_le_seminorm_real [IsTopologicalAddGroup E]72    [Module ℝ E] [ContinuousSMul ℝ E] [PolynormableSpace ℝ E] (S : Subspace ℝ E) (f : Dual ℝ S)73    {p : Seminorm ℝ E} (hp_cont : Continuous p) (hp : ∀ x, f x ≤ p x) :74    ∃ g : StrongDual ℝ E, (∀ x : S, g x = f x) ∧ ∀ x, |g x| ≤ p x := by75  obtain ⟨g, hg, hl⟩ := f.exists_extension_of_le_seminorm_real S hp76  exact ⟨⟨g, (PolynormableSpace.withSeminorms ℝ E).continuous_real_rng g77    ⟨{⟨p, hp_cont⟩}, 1, fun x ↦ by simpa using (le_abs_self _).trans (hl x)⟩⟩, hg, hl⟩7879variable [Module 𝕜 E] [PolynormableSpace 𝕜 E]8081/-- **Hahn-Banach theorem** for linear functionals dominated by a continuous seminorm on82polynormable spaces over fields satisfying `IsRCLikeNormedField`. -/83theorem Module.Dual.exists_continuous_extension_of_le_seminorm (S : Submodule 𝕜 E) (f : Dual 𝕜 S)84    {p : Seminorm 𝕜 E} (hp_cont : Continuous p) (hp : ∀ x, ‖f x‖ ≤ p x) :85    ∃ g : StrongDual 𝕜 E, (∀ x : S, g x = f x) ∧ ∀ x, ‖g x‖ ≤ p x := by86  obtain ⟨g, hg, hle⟩ := Dual.exists_extension_of_le_seminorm S f hp87  refine ⟨⟨g, (PolynormableSpace.withSeminorms 𝕜 E).continuous_normedSpace_rng 𝕜 g ?_⟩, hg, hle⟩88  exact ⟨{⟨p, hp_cont⟩}, 1, by simpa⟩8990/-- **Hahn-Banach theorem** for continuous linear functionals on polynormable spaces over a field91satisfying `IsRCLikeNormedField`. -/92theorem StrongDual.exists_extension {𝕜} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜]93    [Module 𝕜 E] [PolynormableSpace 𝕜 E] (S : Submodule 𝕜 E) (f : StrongDual 𝕜 S) :94    ∃ g : StrongDual 𝕜 E, ∀ x : S, g x = f x := by95  obtain ⟨q, hq_cont, hq⟩ := Seminorm.exists_le_comp_of_isInducing (f := S.subtype)96    (p := f.toSeminorm) f.continuous.norm IsInducing.subtypeVal97  obtain ⟨g, hg, _⟩ := Dual.exists_continuous_extension_of_le_seminorm S f.toLinearMap hq_cont hq98  exact ⟨g, hg⟩99100variable {F : Type*} [AddCommGroup F] [TopologicalSpace F] [IsTopologicalAddGroup F] [Module 𝕜 F]101  [ContinuousSMul 𝕜 F] [T2Space F]102103/-- Corollary of the polynormable **Hahn-Banach theorem**: if `f : S → F` is a continuous104linear map with finite-dimensional range, then `f` extends to a continuous linear map on the whole105space. -/106lemma ContinuousLinearMap.exist_extension_of_finiteDimensional_range {S : Submodule 𝕜 E}107    (f : S →L[𝕜] F) [FiniteDimensional 𝕜 f.range] :108    ∃ g : E →L[𝕜] F, f = g.comp S.subtypeL := by109  letI : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜110  let b := Module.finBasis 𝕜 f.range111  let e := b.equivFunL112  let fi := fun i ↦ (LinearMap.toContinuousLinearMap (b.coord i)).comp113    (f.codRestrict _ <| LinearMap.mem_range_self _)114  choose gi hgf using fun i ↦ StrongDual.exists_extension S (fi i)115  use f.range.subtypeL.comp <| e.symm.toContinuousLinearMap.comp (.pi gi)116  ext x117  simp [fi, e, hgf]118119/-- A finite-dimensional submodule of a polynormable space over a field satisfying120`IsRCLikeNormedField` is `Submodule.ClosedComplemented`. -/121lemma Submodule.ClosedComplemented.of_finiteDimensional [PolynormableSpace 𝕜 F] (S : Submodule 𝕜 F)122    [FiniteDimensional 𝕜 S] : S.ClosedComplemented := by123  let ⟨g, hg⟩ := (ContinuousLinearMap.id 𝕜 S).exist_extension_of_finiteDimensional_range124  exact ⟨g, DFunLike.congr_fun hg.symm⟩