The Grassmannians of a Banach space

Lax606786.BanachGrassmannian · concepts/Lax606786/BanachGrassmannian.lean · lax-606786

definition

Loading review…

Natural Language Statement

Definition

Let $X$ be a real normed space. The unit sphere of a subspace $V \le X$ is $\mathbb{S}_V = \{x \in V : \|x\| = 1\}$ ; it spans $V$ , so it determines $V$ .

The Grassmannian $\mathcal{G} X$ is the set of closed subspaces $V \le X$ admitting a bounded projection $X \to V$ . It carries the distance $d(V, W) = d_H(\mathbb{S}_V, \mathbb{S}_W) \in [0, \infty],$ the Hausdorff distance between unit spheres (infinite exactly when one of $V, W$ is $0$ and the other is not).
For $k \ge 0$ , $\mathcal{G}^k X$ is the set of $V \in \mathcal{G} X$ of codimension $k$ , that is, with $\dim(X/V) = k$ .
For $k \ge 0$ , $\mathcal{G}_k X$ is the set of $k$ -dimensional subspaces of $X$ . For $k \ge 1$ the unit sphere $\mathbb{S}_V$ is a nonempty compact set and $\mathcal{G}_k X$ carries the metric $d(V, W) = d_H(\mathbb{S}_V, \mathbb{S}_W)$ .

Each is equipped with the Borel $\sigma$ -algebra of its distance.

Concept map

1 concept

100%

DefinitionThis conceptDescendants are omitted for concepts with more than 10 descendants.

In the paper

page 3 of this submission's paper

Lean source view on GitLab

Show types on hover

1	import Mathlib.Analysis.RCLike.Lemmas
2	import Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
3	import Mathlib.Topology.MetricSpace.Closeds
4	import Mathlib.Analysis.LocallyConvex.HahnBanach
5	import Mathlib.Analysis.Normed.Module.HahnBanach
6
7	/-!
8	---
9	title: The Grassmannians of a Banach space
10	type: definition
11	---
12	Let $X$ be a real normed space. The unit sphere of a subspace $V \le X$ is
13	$\mathbb{S}_V = \{x \in V : \\|x\\| = 1\}$ ; it spans $V$ , so it determines $V$ .
14
15	- The Grassmannian $\mathcal{G} X$ is the set of closed subspaces $V \le X$ admitting a bounded
16	projection $X \to V$ . It carries the distance
17	$d(V, W) = d_H(\mathbb{S}_V, \mathbb{S}_W) \in [0, \infty],$
18	the Hausdorff distance between unit spheres (infinite exactly when one of $V, W$ is $0$ and
19	the other is not).
20	- For $k \ge 0$ , $\mathcal{G}^k X$ is the set of $V \in \mathcal{G} X$ of codimension $k$ , that
21	is, with $\dim(X/V) = k$ .
22	- For $k \ge 0$ , $\mathcal{G}_k X$ is the set of $k$ -dimensional subspaces of $X$ . For
23	$k \ge 1$ the unit sphere $\mathbb{S}_V$ is a nonempty compact set and $\mathcal{G}_k X$
24	carries the metric $d(V, W) = d_H(\mathbb{S}_V, \mathbb{S}_W)$ .
25
26	Each is equipped with the Borel $\sigma$ -algebra of its distance.
27	-/
28
29	namespace Lax606786.BanachGrassmannian
30
31	open TopologicalSpace
32
33	variable (X : Type*) [NormedAddCommGroup X] [NormedSpace ℝ X]
34
35	/-- `𝒢X`: the closed subspaces of `X` admitting a bounded projection onto them. -/
36	def Grassmannian : Type _ :=
37	{V : Submodule ℝ X // V.ClosedComplemented}
38
39	variable {X}
40
41	/-- Every subspace is spanned by its unit sphere. -/
42	theorem span_sphere_inter (V : Submodule ℝ X) :
43	Submodule.span ℝ (Metric.sphere (0 : X) 1 ∩ (V : Set X)) = V := by
44	apply le_antisymm
45	· exact Submodule.span_le.2 Set.inter_subset_right
46	· intro x hx
47	rcases eq_or_ne x 0 with rfl \| hx0
48	· exact Submodule.zero_mem _
49	· have hxeq : x = ‖x‖ • (‖x‖⁻¹ • x) := by
50	rw [smul_smul, mul_inv_cancel₀ (norm_ne_zero_iff.2 hx0), one_smul]
51	rw [hxeq]
52	refine Submodule.smul_mem _ _ (Submodule.subset_span ⟨?_, V.smul_mem _ hx⟩)
53	rw [mem_sphere_zero_iff_norm, norm_smul, norm_inv, norm_norm,
54	inv_mul_cancel₀ (norm_ne_zero_iff.2 hx0)]
55
56	namespace Grassmannian
57
58	/-- The unit sphere `𝕊_V = {x ∈ V : ‖x‖ = 1}`. -/
59	def sphere (V : Grassmannian X) : Set X :=
60	Metric.sphere (0 : X) 1 ∩ (V.1 : Set X)
61
62	/-- `V ↦ 𝕊_V`, as a closed subset of `X`. -/
63	def toCloseds (V : Grassmannian X) : Closeds X :=
64	⟨V.sphere, Metric.isClosed_sphere.inter V.2.isClosed⟩
65
66	/-- A subspace is the span of its unit sphere, so `V ↦ 𝕊_V` is injective. -/
67	theorem toCloseds_injective : Function.Injective (toCloseds (X := X)) := by
68	intro V W h
69	apply Subtype.ext
70	rw [← span_sphere_inter V.1, ← span_sphere_inter W.1]
71	exact congrArg (fun s : Closeds X => Submodule.span ℝ (s : Set X)) h
72
73	/-- The distance on `𝒢X`: the Hausdorff distance between unit spheres. -/
74	noncomputable instance instEMetricSpace : EMetricSpace (Grassmannian X) :=
75	EMetricSpace.induced toCloseds toCloseds_injective inferInstance
76
77	/-- The Borel `σ`-algebra of that distance. -/
78	noncomputable instance instMeasurableSpace : MeasurableSpace (Grassmannian X) :=
79	borel (Grassmannian X)
80
81	instance instBorelSpace : BorelSpace (Grassmannian X) := ⟨rfl⟩
82
83	/-- `𝕊_V` is closed. -/
84	theorem isClosed_sphere (V : Grassmannian X) : IsClosed V.sphere :=
85	Metric.isClosed_sphere.inter V.2.isClosed
86
87	end Grassmannian
88
89	variable (X)
90
91	/-- `𝒢^k X`: the subspaces in `𝒢X` of codimension `k`. -/
92	def GrassmannianCofin (k : ℕ) : Type _ :=
93	{V : Grassmannian X // FiniteDimensional ℝ (X ⧸ (V.1 : Submodule ℝ X)) ∧
94	Module.finrank ℝ (X ⧸ (V.1 : Submodule ℝ X)) = k}
95
96	/-- `𝒢_k X`: the `k`-dimensional subspaces of `X`. -/
97	def GrassmannianFin (k : ℕ) : Type _ :=
98	{V : Submodule ℝ X // FiniteDimensional ℝ V ∧ Module.finrank ℝ V = k}
99
100	variable {X}
101
102	namespace GrassmannianFin
103
104	/-- The unit sphere `𝕊_V = {x ∈ V : ‖x‖ = 1}`. -/
105	def sphere {k : ℕ} (V : GrassmannianFin X k) : Set X :=
106	Metric.sphere (0 : X) 1 ∩ (V.1 : Set X)
107
108	/-- `V` is the span of its unit sphere. -/
109	theorem span_sphere {k : ℕ} (V : GrassmannianFin X k) :
110	Submodule.span ℝ V.sphere = (V.1 : Submodule ℝ X) := by
111	apply le_antisymm
112	· exact Submodule.span_le.2 Set.inter_subset_right
113	· intro x hx
114	rcases eq_or_ne x 0 with rfl \| hx0
115	· exact Submodule.zero_mem _
116	· have hxeq : x = ‖x‖ • (‖x‖⁻¹ • x) := by
117	rw [smul_smul, mul_inv_cancel₀ (norm_ne_zero_iff.2 hx0), one_smul]
118	rw [hxeq]
119	refine Submodule.smul_mem _ _ (Submodule.subset_span ⟨?_, V.1.smul_mem _ hx⟩)
120	rw [mem_sphere_zero_iff_norm, norm_smul, norm_inv, norm_norm,
121	inv_mul_cancel₀ (norm_ne_zero_iff.2 hx0)]
122
123	/-- `𝕊_V` is compact. -/
124	theorem isCompact_sphere {k : ℕ} (V : GrassmannianFin X k) : IsCompact V.sphere := by
125	have : FiniteDimensional ℝ (V.1 : Submodule ℝ X) := V.2.1
126	have himg : V.sphere =
127	(Subtype.val : (V.1 : Submodule ℝ X) → X) '' Metric.sphere (0 : (V.1 : Submodule ℝ X)) 1 := by
128	ext x
129	simp only [sphere, Set.mem_inter_iff, Set.mem_image]
130	constructor
131	· rintro ⟨hx1, hxV⟩
132	refine ⟨⟨x, hxV⟩, ?_, rfl⟩
133	rwa [mem_sphere_zero_iff_norm] at hx1 ⊢
134	· rintro ⟨v, hv, rfl⟩
135	rw [mem_sphere_zero_iff_norm] at hv
136	exact ⟨by rwa [mem_sphere_zero_iff_norm], v.2⟩
137	rw [himg]
138	exact (_root_.isCompact_sphere (0 : (V.1 : Submodule ℝ X)) 1).image continuous_subtype_val
139
140	/-- `𝕊_V` is nonempty when `k ≠ 0`. -/
141	theorem nonempty_sphere {k : ℕ} [NeZero k] (V : GrassmannianFin X k) : V.sphere.Nonempty := by
142	have hne : (V.1 : Submodule ℝ X) ≠ ⊥ := by
143	intro h
144	apply NeZero.ne k
145	have hfr := V.2.2
146	rw [h, finrank_bot] at hfr
147	exact hfr.symm
148	obtain ⟨x, hxV, hx0⟩ := Submodule.exists_mem_ne_zero_of_ne_bot hne
149	refine ⟨‖x‖⁻¹ • x, ?_, V.1.smul_mem _ hxV⟩
150	rw [mem_sphere_zero_iff_norm, norm_smul, norm_inv, norm_norm,
151	inv_mul_cancel₀ (norm_ne_zero_iff.2 hx0)]
152
153	/-- `V ↦ 𝕊_V`, as a nonempty compact subset of `X`. -/
154	noncomputable def toNonemptyCompacts {k : ℕ} [NeZero k] (V : GrassmannianFin X k) :
155	NonemptyCompacts X where
156	carrier := V.sphere
157	isCompact' := V.isCompact_sphere
158	nonempty' := V.nonempty_sphere
159
160	/-- A subspace is the span of its unit sphere, so `V ↦ 𝕊_V` is injective. -/
161	theorem toNonemptyCompacts_injective (k : ℕ) [NeZero k] :
162	Function.Injective (toNonemptyCompacts (X := X) (k := k)) := by
163	intro V W h
164	apply Subtype.ext
165	rw [← V.span_sphere, ← W.span_sphere]
166	exact congrArg (fun s : NonemptyCompacts X => Submodule.span ℝ (s : Set X)) h
167
168	/-- The metric on `𝒢_k X`: the Hausdorff distance between unit spheres. -/
169	noncomputable instance instMetricSpace (k : ℕ) [NeZero k] : MetricSpace (GrassmannianFin X k) :=
170	MetricSpace.induced toNonemptyCompacts (toNonemptyCompacts_injective k) inferInstance
171
172	/-- The Borel `σ`-algebra of that metric. -/
173	noncomputable instance instMeasurableSpace (k : ℕ) [NeZero k] :
174	MeasurableSpace (GrassmannianFin X k) :=
175	borel (GrassmannianFin X k)
176
177	instance instBorelSpace (k : ℕ) [NeZero k] : BorelSpace (GrassmannianFin X k) := ⟨rfl⟩
178
179	/-- `V` is recovered from `𝕊_V`. -/
180	theorem sphere_injective (k : ℕ) : Function.Injective (sphere (X := X) (k := k)) := by
181	intro V W h
182	apply Subtype.ext
183	rw [← V.span_sphere, ← W.span_sphere, h]
184
185	/-- A finite-dimensional subspace admits a bounded projection onto it, so `𝒢_k X` sits inside
186	`𝒢 X`. -/
187	theorem closedComplemented {k : ℕ} (V : GrassmannianFin X k) :
188	(V.1 : Submodule ℝ X).ClosedComplemented := by
189	have : FiniteDimensional ℝ (V.1 : Submodule ℝ X) := V.2.1
190	exact Submodule.ClosedComplemented.of_finiteDimensional _
191
192	/-- The inclusion `𝒢_k X → 𝒢 X`. -/
193	def toGrassmannian {k : ℕ} (V : GrassmannianFin X k) : Grassmannian X :=
194	⟨V.1, V.closedComplemented⟩
195
196	end GrassmannianFin
197
198	end Lax606786.BanachGrassmannian
199

Builds on

none

Used by

From Mathlib

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

Loading discussion…

Lax Lean Archive

The Grassmannians of a Banach space

Flags

Flag this concept

Natural Language Statement

Definition

In the paper

Lean source view on GitLab

Discussion

Settings

Your comments