Skip to content

Commit b657502

Browse files
CoolRmalpre-commit-ci-lite[bot]
CoolRmal
and
pre-commit-ci-lite[bot]
committed
feat: Analytic Hahn Banach theorem for locally convex spaces (leanprover-community#38739)
Closes leanprover-community#38419 This PR proves Hahn-Banach theorem for locally convex spaces, which allow us to generalize both [ContinuousLinearMap.exist_extension_of_finiteDimensional_range](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Normed/Module/HahnBanach.html#ContinuousLinearMap.exist_extension_of_finiteDimensional_range) and [Submodule.ClosedComplemented.of_finiteDimensional](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Normed/Module/HahnBanach.html#Submodule.ClosedComplemented.of_finiteDimensional) (I also moved these two lemmas to the new file I created). Some helper lemmas about continuity of seminorms/linear functions are added. Created with the help of Codex. Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com> Co-authored-by: Yongxi Lin <aaronlin@andrew.cmu.edu> Co-authored-by: Yongxi(Aaron) Lin <aaronlin@andrew.cmu.edu>
1 parent 8205572 commit b657502

6 files changed

Lines changed: 227 additions & 117 deletions

File tree

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2067,6 +2067,7 @@ public import Mathlib.Analysis.LocallyConvex.Barrelled
20672067
public import Mathlib.Analysis.LocallyConvex.Basic
20682068
public import Mathlib.Analysis.LocallyConvex.Bounded
20692069
public import Mathlib.Analysis.LocallyConvex.ContinuousOfBounded
2070+
public import Mathlib.Analysis.LocallyConvex.HahnBanach
20702071
public import Mathlib.Analysis.LocallyConvex.Montel
20712072
public import Mathlib.Analysis.LocallyConvex.PointwiseConvergence
20722073
public import Mathlib.Analysis.LocallyConvex.Polar

‎Mathlib/Analysis/LocallyConvex/HahnBanach.lean‎

Lines changed: 124 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,124 @@
1+
/-
2+
Copyright (c) 2026 Yongxi Lin. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Yongxi Lin
5+
-/
6+
module
7+
8+
public import Mathlib.Analysis.Convex.Cone.Extension
9+
public import Mathlib.Analysis.LocallyConvex.AbsConvexOpen
10+
public import Mathlib.Analysis.LocallyConvex.WeakDual
11+
public import Mathlib.Analysis.Normed.Module.RCLike.Extend
12+
public import Mathlib.Topology.Algebra.Module.FiniteDimension
13+
14+
/-!
15+
# Hahn-Banach theorem for polynormable spaces
16+
17+
In this file, we prove the analytic Hahn-Banach theorem for polynormable spaces over a field
18+
satisfying `IsRCLikeNormedField`. For any continuous linear functional on a subspace, we can extend
19+
it to the entire space. Note that we cannot use `LocallyConvexSpace` because an
20+
`IsRCLikeNormedField` has no order structure.
21+
22+
We prove
23+
* `Module.Dual.exists_continuous_extension_of_le_seminorm`: Hahn-Banach theorem for linear
24+
functionals dominated by a continuous seminorm on polynormable spaces over a field satisfying
25+
`IsRCLikeNormedField`.
26+
* `StrongDual.exists_extension`: Hahn-Banach theorem for continuous linear functionals on
27+
polynormable spaces over fields satisfying `IsRCLikeNormedField`.
28+
29+
-/
30+
31+
public section
32+
33+
open Module Topology RCLike
34+
35+
open scoped ComplexConjugate
36+
37+
variable {𝕜 E : Type*} [AddCommGroup E]
38+
39+
theorem 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 := by
43+
obtain ⟨g, hg, hl⟩ := by
44+
refine exists_extension_of_le_sublinear ⟨S, f⟩ p (fun _ hc _ => ?_) ?_ hp
45+
· simp [map_smul_eq_mul, abs_of_nonneg hc.le]
46+
· exact fun x y => map_add_le_add p x y
47+
exact ⟨g, hg, p.abs_le_of_le hl⟩
48+
49+
variable [NormedField 𝕜] [IsRCLikeNormedField 𝕜]
50+
51+
theorem 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 := by
54+
letI : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
55+
letI : Module ℝ E := .restrictScalars ℝ 𝕜 E
56+
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_seminorm
65+
exact hgp
66+
67+
variable [TopologicalSpace E]
68+
69+
/-- **Hahn-Banach theorem** for linear functionals dominated by a continuous seminorm on
70+
polynormable spaces over `ℝ`. -/
71+
theorem 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 := by
75+
obtain ⟨g, hg, hl⟩ := f.exists_extension_of_le_seminorm_real S hp
76+
exact ⟨⟨g, (PolynormableSpace.withSeminorms ℝ E).continuous_real_rng g
77+
⟨{⟨p, hp_cont⟩}, 1, fun x ↦ by simpa using (le_abs_self _).trans (hl x)⟩⟩, hg, hl⟩
78+
79+
variable [Module 𝕜 E] [PolynormableSpace 𝕜 E]
80+
81+
/-- **Hahn-Banach theorem** for linear functionals dominated by a continuous seminorm on
82+
polynormable spaces over fields satisfying `IsRCLikeNormedField`. -/
83+
theorem 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 := by
86+
obtain ⟨g, hg, hle⟩ := Dual.exists_extension_of_le_seminorm S f hp
87+
refine ⟨⟨g, (PolynormableSpace.withSeminorms 𝕜 E).continuous_normedSpace_rng 𝕜 g ?_⟩, hg, hle⟩
88+
exact ⟨{⟨p, hp_cont⟩}, 1, by simpa⟩
89+
90+
/-- **Hahn-Banach theorem** for continuous linear functionals on polynormable spaces over a field
91+
satisfying `IsRCLikeNormedField`. -/
92+
theorem 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 := by
95+
obtain ⟨q, hq_cont, hq⟩ := Seminorm.exists_le_comp_of_isInducing (f := S.subtype)
96+
(p := f.toSeminorm) f.continuous.norm IsInducing.subtypeVal
97+
obtain ⟨g, hg, _⟩ := Dual.exists_continuous_extension_of_le_seminorm S f.toLinearMap hq_cont hq
98+
exact ⟨g, hg⟩
99+
100+
variable {F : Type*} [AddCommGroup F] [TopologicalSpace F] [IsTopologicalAddGroup F] [Module 𝕜 F]
101+
[ContinuousSMul 𝕜 F] [T2Space F]
102+
103+
/-- Corollary of the polynormable **Hahn-Banach theorem**: if `f : S → F` is a continuous
104+
linear map with finite-dimensional range, then `f` extends to a continuous linear map on the whole
105+
space. -/
106+
lemma 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 := by
109+
letI : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
110+
let b := Module.finBasis 𝕜 f.range
111+
let e := b.equivFunL
112+
let fi := fun i ↦ (LinearMap.toContinuousLinearMap (b.coord i)).comp
113+
(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 x
117+
simp [fi, e, hgf]
118+
119+
/-- A finite-dimensional submodule of a polynormable space over a field satisfying
120+
`IsRCLikeNormedField` is `Submodule.ClosedComplemented`. -/
121+
lemma Submodule.ClosedComplemented.of_finiteDimensional [PolynormableSpace 𝕜 F] (S : Submodule 𝕜 F)
122+
[FiniteDimensional 𝕜 S] : S.ClosedComplemented := by
123+
let ⟨g, hg⟩ := (ContinuousLinearMap.id 𝕜 S).exist_extension_of_finiteDimensional_range
124+
exact ⟨g, DFunLike.congr_fun hg.symm⟩

‎Mathlib/Analysis/LocallyConvex/WithSeminorms.lean‎

Lines changed: 43 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -674,14 +674,9 @@ theorem continuous_of_isBounded {p : SeminormFamily 𝕝 E ι} {q : SeminormFami
674674
have : IsTopologicalAddGroup E := hp.topologicalAddGroup
675675
refine continuous_of_continuous_comp hq _ fun i => ?_
676676
rcases hf i with ⟨s, C, hC⟩
677-
rw [← Seminorm.finset_sup_smul] at hC
678-
-- Note: we deduce continuity of `s.sup (C • p)` from that of `∑ i ∈ s, C • p i`.
679-
-- The reason is that there is no `continuous_finset_sup`, and even if it were we couldn't
680-
-- really use it since `ℝ` is not an `OrderBot`.
681-
refine Seminorm.continuous_of_le ?_ (hC.trans <| Seminorm.finset_sup_le_sum _ _)
682-
change Continuous (fun x ↦ Seminorm.coeFnAddMonoidHom _ _ (∑ i ∈ s, C • p i) x)
683-
simp_rw [map_sum, Finset.sum_apply]
684-
exact (continuous_finsetSum _ fun i _ ↦ (hp.continuous_seminorm i).const_smul (C : ℝ))
677+
rw [← finset_sup_smul] at hC
678+
exact continuous_of_le
679+
(continuous_finsetSup fun i _ ↦ (hp.continuous_seminorm i).const_smul C) hC
685680

686681
@[deprecated (since := "2026-03-09")]
687682
alias _root_.Seminorm.continuous_from_bounded := continuous_of_isBounded
@@ -693,6 +688,18 @@ theorem continuous_normedSpace_rng (F) [SeminormedAddCommGroup F] [NormedSpace
693688
rw [← Seminorm.isBounded_const (Fin 1)] at hf
694689
exact continuous_of_isBounded hp (norm_withSeminorms 𝕝₂ F) f hf
695690

691+
lemma _root_.Seminorm.abs_le_of_le [Module ℝ E] {p : Seminorm ℝ E}
692+
{f : E →ₗ[ℝ] ℝ} (hfp : ∀ x, f x ≤ p x) (x : E) :
693+
|f x| ≤ p x :=
694+
abs_le.2 ⟨neg_le.1 (by simpa using hfp (-x)), hfp x⟩
695+
696+
theorem continuous_real_rng [Module ℝ E] [TopologicalSpace E] {p : ι → Seminorm ℝ E}
697+
(hp : WithSeminorms p) (f : E →ₗ[ℝ] ℝ)
698+
(hf : ∃ (s : Finset ι) (C : ℝ≥0), ∀ x, f x ≤ (C • s.sup p) x) :
699+
Continuous f := by
700+
obtain ⟨s, C, hC⟩ := hf
701+
exact continuous_normedSpace_rng ℝ hp f ⟨s, C, abs_le_of_le hC⟩
702+
696703
@[deprecated (since := "2026-03-09")]
697704
alias _root_.Seminorm.cont_withSeminorms_normedSpace := continuous_normedSpace_rng
698705

@@ -966,6 +973,12 @@ theorem SeminormFamily.comp_apply (q : SeminormFamily 𝕜₂ F ι) (i : ι) (f
966973
q.comp f i = (q i).comp f :=
967974
rfl
968975

976+
theorem SeminormFamily.comp_smul_nnreal (q : SeminormFamily 𝕜₂ F ι) (c : NNReal)
977+
(f : E →ₛₗ[σ₁₂] F) :
978+
c • q.comp f = (c • q).comp f := by
979+
ext
980+
simp [SeminormFamily.comp_apply, Seminorm.comp_apply]
981+
969982
theorem SeminormFamily.finset_sup_comp (q : SeminormFamily 𝕜₂ F ι) (s : Finset ι)
970983
(f : E →ₛₗ[σ₁₂] F) : (s.sup q).comp f = s.sup (q.comp f) := by
971984
ext x
@@ -1005,6 +1018,28 @@ instance [PolynormableSpace 𝕜₂ F] {S : Submodule 𝕜₂ F} :
10051018
PolynormableSpace 𝕜₂ S :=
10061019
IsInducing.polynormableSpace (f := S.subtype) .subtypeVal
10071020

1021+
section NontriviallyNormedField
1022+
1023+
variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] [Module 𝕜 E] [TopologicalSpace E]
1024+
variable {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂]
1025+
1026+
theorem Seminorm.bound_comp_of_isInducing {p : Seminorm 𝕜 E} (hp : Continuous p)
1027+
{q : SeminormFamily 𝕜₂ F ι} (hq : WithSeminorms q) {f : E →ₛₗ[σ₁₂] F} (hf : IsInducing f) :
1028+
∃ (s : Finset ι) (C : ℝ≥0), C ≠ 0 ∧ p ≤ (C • s.sup q).comp f := by
1029+
obtain ⟨s, C, hC, hqC⟩ := Seminorm.bound_of_continuous (hf.withSeminorms hq) p hp
1030+
rw [← SeminormFamily.finset_sup_comp, ← Seminorm.smul_comp] at hqC
1031+
exact ⟨s, C, hC, hqC⟩
1032+
1033+
theorem Seminorm.exists_le_comp_of_isInducing {p : Seminorm 𝕜 E} (hp : Continuous p)
1034+
[PolynormableSpace 𝕜₂ F] {f : E →ₛₗ[σ₁₂] F} (hf : IsInducing f) :
1035+
∃ p₂ : Seminorm 𝕜₂ F, Continuous p₂ ∧ p ≤ p₂.comp f := by
1036+
obtain ⟨s, C, -, hqC⟩ := Seminorm.bound_comp_of_isInducing hp
1037+
(PolynormableSpace.withSeminorms 𝕜₂ F) hf
1038+
have := (PolynormableSpace.withSeminorms 𝕜₂ F).topologicalAddGroup
1039+
exact ⟨_, Continuous.const_smul (continuous_finsetSup fun i _ => i.2) C, hqC⟩
1040+
1041+
end NontriviallyNormedField
1042+
10081043
/-- (Disjoint) union of seminorm families. -/
10091044
protected def SeminormFamily.sigma {κ : ι → Type*} (p : (i : ι) → SeminormFamily 𝕜 E (κ i)) :
10101045
SeminormFamily 𝕜 E ((i : ι) × κ i) :=

‎Mathlib/Analysis/Normed/Module/HahnBanach.lean‎

Lines changed: 15 additions & 95 deletions
Original file line numberDiff line numberDiff line change
@@ -5,21 +5,19 @@ Authors: Yury Kudryashov, Heather Macbeth
55
-/
66
module
77

8-
public import Mathlib.Analysis.Convex.Cone.Extension
9-
public import Mathlib.Analysis.Normed.Module.RCLike.Extend
10-
public import Mathlib.Analysis.RCLike.Lemmas
11-
public import Mathlib.Topology.Algebra.Module.Complement
8+
public import Mathlib.Analysis.LocallyConvex.HahnBanach
9+
public import Mathlib.Analysis.Normed.Module.Span
1210

1311
/-!
14-
# Extension Hahn-Banach theorem
12+
# Hahn-Banach extension theorem
1513
16-
In this file we prove the analytic Hahn-Banach theorem. For any continuous linear function on a
17-
subspace, we can extend it to a function on the entire space without changing its norm.
14+
In this file, we prove the analytic Hahn-Banach theorem for normed vector spaces. For any continuous
15+
linear functional on a subspace, we can extend it to the entire space without changing
16+
its norm. For Hahn-Banach theorems for locally convex spaces, see
17+
`Mathlib.Analysis.LocallyConvex.HahnBanach`.
1818
1919
We prove
20-
* `Real.exists_extension_norm_eq`: Hahn-Banach theorem for continuous linear functions on normed
21-
spaces over `ℝ`.
22-
* `exists_extension_norm_eq`: Hahn-Banach theorem for continuous linear functions on normed spaces
20+
* `exists_extension_norm_eq`: Hahn-Banach theorem for continuous linear functionals on normed spaces
2321
over `ℝ` or `ℂ`.
2422
2523
In order to state and prove the corollaries uniformly, we prove the statements for a field `𝕜`
@@ -35,102 +33,24 @@ public section
3533

3634
universe u v
3735

38-
namespace Real
39-
40-
variable {E : Type*} [SeminormedAddCommGroup E] [NormedSpace ℝ E]
41-
42-
/-- **Hahn-Banach theorem** for continuous linear functions over `ℝ`.
43-
See also `exists_extension_norm_eq` in the root namespace for a more general version
44-
that works both for `ℝ` and `ℂ`. -/
45-
theorem exists_extension_norm_eq (p : Subspace ℝ E) (f : StrongDual ℝ p) :
46-
∃ g : StrongDual ℝ E, (∀ x : p, g x = f x) ∧ ‖g‖ = ‖f‖ := by
47-
rcases exists_extension_of_le_sublinear ⟨p, f⟩ (fun x => ‖f‖ * ‖x‖)
48-
(fun c hc x => by simp only [norm_smul c x, Real.norm_eq_abs, abs_of_pos hc, mul_left_comm])
49-
(fun x y => by
50-
rw [← left_distrib]
51-
gcongr
52-
exact norm_add_le x y)
53-
fun x => le_trans (le_abs_self _) (f.le_opNorm _) with ⟨g, g_eq, g_le⟩
54-
set g' :=
55-
g.mkContinuous ‖f‖ fun x => abs_le.2 ⟨neg_le.1 <| g.map_neg x ▸ norm_neg x ▸ g_le (-x), g_le x⟩
56-
refine ⟨g', g_eq, ?_⟩
57-
apply le_antisymm (g.mkContinuous_norm_le (norm_nonneg f) _)
58-
refine f.opNorm_le_bound (norm_nonneg _) fun x => ?_
59-
dsimp at g_eq
60-
rw [← g_eq]
61-
apply g'.le_opNorm
62-
63-
end Real
64-
6536
section RCLike
6637

6738
open RCLike
6839

69-
variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] {E F : Type*}
40+
variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] {E : Type*}
7041
[SeminormedAddCommGroup E] [NormedSpace 𝕜 E]
71-
[NormedAddCommGroup F] [NormedSpace 𝕜 F]
7242

7343
/-- **Hahn-Banach theorem** for continuous linear functions over `𝕜`
7444
satisfying `IsRCLikeNormedField 𝕜`. -/
7545
@[wikidata Q866116]
7646
theorem exists_extension_norm_eq (p : Subspace 𝕜 E) (f : StrongDual 𝕜 p) :
7747
∃ g : StrongDual 𝕜 E, (∀ x : p, g x = f x) ∧ ‖g‖ = ‖f‖ := by
78-
letI : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
79-
letI : Module ℝ E := .restrictScalars ℝ 𝕜 E
80-
haveI : IsScalarTower ℝ 𝕜 E := .restrictScalars _ _ _
81-
letI : NormedSpace ℝ E := NormedSpace.restrictScalars _ 𝕜 _
82-
-- Let `fr: StrongDual ℝ p` be the real part of `f`.
83-
let fr := reCLM.comp (f.restrictScalars ℝ)
84-
-- Use the real version to get a norm-preserving extension of `fr`, which
85-
-- we'll call `g : StrongDual ℝ E`.
86-
-- the type ascription on `hextends` is necessary to make sure the quantification
87-
-- happens over `x : p` instead of `x : p.restrictScalars ℝ`.
88-
obtain ⟨g, ⟨(hextends : ∀ x : p, g x = fr x), hnormeq⟩⟩ :=
89-
Real.exists_extension_norm_eq (p.restrictScalars ℝ) fr
90-
-- Now `g` can be extended to the `StrongDual 𝕜 E` we need.
91-
refine ⟨g.extendRCLike, ?_⟩
92-
-- It is an extension of `f`.
93-
have h (x : p) : g.extendRCLike x = f x := by
94-
rw [g.extendRCLike_apply, ← Submodule.coe_smul,
95-
hextends, hextends]
96-
simp [fr, RCLike.algebraMap_eq_ofReal, mul_comm I, RCLike.re_add_im]
97-
-- And we derive the equality of the norms by bounding on both sides.
98-
refine ⟨h, le_antisymm ?_ ?_⟩
99-
· calc
100-
‖g.extendRCLike‖ = ‖g‖ := g.norm_extendRCLike
101-
_ = ‖fr‖ := hnormeq
102-
_ ≤ ‖reCLM‖ * ‖f‖ := ContinuousLinearMap.opNorm_comp_le _ _
103-
_ = ‖f‖ := by rw [reCLM_norm, one_mul]
104-
· exact f.opNorm_le_bound (g.extendRCLike (𝕜 := 𝕜)).opNorm_nonneg
105-
fun x ↦ h x ▸ (g.extendRCLike (𝕜 := 𝕜) |>.le_opNorm x)
106-
107-
open Module
108-
109-
/-- Corollary of the **Hahn-Banach theorem**: if `f : p → F` is a continuous linear map
110-
from a submodule of a normed space `E` over `𝕜`, `𝕜 = ℝ` or `𝕜 = ℂ`,
111-
with a finite-dimensional range, then `f` admits an extension to a continuous linear map `E → F`.
112-
113-
Note that contrary to the case `F = 𝕜`, see `exists_extension_norm_eq`,
114-
we provide no estimates on the norm of the extension.
115-
-/
116-
lemma ContinuousLinearMap.exist_extension_of_finiteDimensional_range {p : Submodule 𝕜 E}
117-
(f : p →L[𝕜] F) [FiniteDimensional 𝕜 f.range] :
118-
∃ g : E →L[𝕜] F, f = g.comp p.subtypeL := by
119-
letI : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
120-
set b := Module.finBasis 𝕜 f.range
121-
set e := b.equivFunL
122-
set fi := fun i ↦ (LinearMap.toContinuousLinearMap (b.coord i)).comp
123-
(f.codRestrict _ <| LinearMap.mem_range_self _)
124-
choose gi hgf _ using fun i ↦ exists_extension_norm_eq p (fi i)
125-
use f.range.subtypeL.comp <| e.symm.toContinuousLinearMap.comp (.pi gi)
126-
ext x
127-
simp [fi, e, hgf]
128-
129-
/-- A finite-dimensional submodule over `ℝ` or `ℂ` is `Submodule.ClosedComplemented`. -/
130-
lemma Submodule.ClosedComplemented.of_finiteDimensional (p : Submodule 𝕜 F)
131-
[FiniteDimensional 𝕜 p] : p.ClosedComplemented :=
132-
let ⟨g, hg⟩ := (ContinuousLinearMap.id 𝕜 p).exist_extension_of_finiteDimensional_range
133-
⟨g, DFunLike.congr_fun hg.symm⟩
48+
obtain ⟨g, hg, hl⟩ := by
49+
refine Module.Dual.exists_continuous_extension_of_le_seminorm p f
50+
(show Continuous (‖f‖₊ • (normSeminorm 𝕜 E)) from ?_) fun x => f.le_opNorm x
51+
exact continuous_norm.const_smul ‖f‖₊
52+
refine ⟨g, hg, le_antisymm (g.opNorm_le_bound (norm_nonneg f) hl) ?_⟩
53+
exact f.opNorm_le_bound (norm_nonneg _) fun x => by simpa [hg x] using g.le_opNorm x
13454

13555
end RCLike
13656

0 commit comments

Comments
 (0)