The Grassmannians of a Banach space

Lax606786.Grassmannian · concepts/Lax606786/Grassmannian.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 $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; 10 descendants hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

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

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