TopologyUnconditional.lean

1 import KomorebiVerification.TopologicalCompletion
2 import Mathlib.Analysis.Normed.Operator.BanachSteinhaus
3 import Mathlib.Analysis.Normed.Module.DoubleDual
4 import Mathlib.Analysis.Normed.Module.FiniteDimension
5 
6 /-! # The general unconditional sum norm -/
7 
8 noncomputable section
9 open scoped BigOperators
10 open Set Function Filter Topology
11 
12 namespace PaperIRelease.TopologyUnconditional
13 
14 variable {𝕜 X : Type*} [RCLike 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X]
15 
16 /-- A finite collection of coefficients from the scalar closed unit ball. -/
17 def Coefficients (𝕜 : Type*) [RCLike 𝕜] :=
18   Finset ℕ × {a : ℕ → 𝕜 // ∀ n, ‖a n‖ ≤ 1}
19 
20 def finiteSum (x : ℕ → X) (c : Coefficients 𝕜) : X :=
21   ∑ n ∈ c.1, c.2.val n • x n
22 
23 /-- Unconditional summability bounds every finite unit-ball multiplier sum.
24 The proof applies uniform boundedness on the continuous dual, whose scalar
25 images are absolutely summable, and then the isometric double-dual embedding. -/
26 theorem summable_finiteSum_bounded (x : ℕ → X) (hx : Summable x) :
27     ∃ C : ℝ, ∀ c : Coefficients 𝕜, ‖finiteSum x c‖ ≤ C := by
28   let g : Coefficients 𝕜 → StrongDual 𝕜 (StrongDual 𝕜 X) :=
29     fun c ↦ NormedSpace.inclusionInDoubleDual 𝕜 X (finiteSum x c)
30   have hpoint : ∀ ℓ : StrongDual 𝕜 X, ∃ C : ℝ, ∀ c, ‖g c ℓ‖ ≤ C := by
31     intro ℓ
32     have hs : Summable (fun n ↦ ‖ℓ (x n)‖) := (ℓ.summable hx).norm
33     refine ⟨∑' n, ‖ℓ (x n)‖, fun c ↦ ?_⟩
34     change ‖ℓ (finiteSum x c)‖ ≤ _
35     simp only [finiteSum, map_sum, map_smul]
36     calc
37       ‖∑ n ∈ c.1, c.2.val n • ℓ (x n)‖ ≤ ∑ n ∈ c.1, ‖c.2.val n • ℓ (x n)‖ :=
38         norm_sum_le _ _
39       _ ≤ ∑ n ∈ c.1, ‖ℓ (x n)‖ := by
40         apply Finset.sum_le_sum
41         intro n _
42         rw [norm_smul]
43         exact mul_le_of_le_one_left (norm_nonneg _) (c.2.property n)
44       _ ≤ ∑' n, ‖ℓ (x n)‖ := hs.sum_le_tsum c.1 (fun _ _ ↦ norm_nonneg _)
45   obtain ⟨C, hC⟩ := banach_steinhaus hpoint
46   refine ⟨C, fun c ↦ ?_⟩
47   have he : ‖g c‖ = ‖finiteSum x c‖ :=
48     (NormedSpace.inclusionInDoubleDualLi 𝕜).norm_map (finiteSum x c)
49   rw [← he]
50   exact hC c
51 
52 /-- A countable family of closed ambient subspaces. -/
53 structure ClosedPackets (𝕜 X : Type*) [RCLike 𝕜]
54     [NormedAddCommGroup X] [NormedSpace 𝕜 X] where
55   packet : ℕ → Submodule 𝕜 X
56   closed : ∀ n, IsClosed (packet n : Set X)
57 
58 namespace ClosedPackets
59 
60 variable (Q : ClosedPackets 𝕜 X)
61 
62 def sequences : Submodule 𝕜 (ℕ → X) where
63   carrier := {x | (∀ n, x n ∈ Q.packet n) ∧ Summable x}
64   zero_mem' := ⟨fun _ ↦ Submodule.zero_mem _, summable_zero⟩
65   add_mem' := by
66     rintro x y ⟨hx, hxs⟩ ⟨hy, hys⟩
67     exact ⟨fun n ↦ Submodule.add_mem _ (hx n) (hy n), hxs.add hys⟩
68   smul_mem' := by
69     rintro c x ⟨hx, hxs⟩
70     exact ⟨fun n ↦ Submodule.smul_mem _ c (hx n), hxs.const_smul c⟩
71 
72 /-- A type synonym separates the signed-sum topology from the product
73 topology on the space of all sequences. -/
74 def Space : Type _ := Q.sequences
75 
76 instance spaceAddCommGroup : AddCommGroup Q.Space :=
77   inferInstanceAs (AddCommGroup Q.sequences)
78 
79 instance spaceModule : Module 𝕜 Q.Space :=
80   inferInstanceAs (Module 𝕜 Q.sequences)
81 
82 @[ext]
83 theorem Space.ext (x y : Q.Space) (h : ∀ n, x.val n = y.val n) : x = y :=
84   Subtype.ext (funext h)
85 
86 @[simp] theorem space_zero_val (n : ℕ) : (0 : Q.Space).val n = 0 := rfl
87 @[simp] theorem space_add_val (x y : Q.Space) (n : ℕ) : (x + y).val n = x.val n + y.val n := rfl
88 @[simp] theorem space_neg_val (x : Q.Space) (n : ℕ) : (-x).val n = -x.val n := rfl
89 @[simp] theorem space_sub_val (x y : Q.Space) (n : ℕ) : (x - y).val n = x.val n - y.val n := rfl
90 @[simp] theorem space_smul_val (a : 𝕜) (x : Q.Space) (n : ℕ) : (a • x).val n = a • x.val n := rfl
91 
92 def signedValues (x : Q.Space) : Set ℝ := range (fun c : Coefficients 𝕜 ↦ ‖finiteSum x.val c‖)
93 
94 theorem signedValues_nonempty (x : Q.Space) : (Q.signedValues x).Nonempty := by
95   refine ⟨0, ⟨∅, ⟨fun _ ↦ 0, by simp⟩⟩, ?_⟩
96   simp [finiteSum]
97 
98 theorem signedValues_bddAbove (x : Q.Space) : BddAbove (Q.signedValues x) := by
99   obtain ⟨C, hC⟩ := summable_finiteSum_bounded (𝕜 := 𝕜) x.val x.property.2
100   exact ⟨C, by rintro v ⟨c, rfl⟩; exact hC c⟩
101 
102 /-- The norm is exactly the supremum printed in the unconditional sum
103 space definition, with no extra boundedness hypothesis on its members. -/
104 def unconditionalNorm (x : Q.Space) : ℝ := sSup (Q.signedValues x)
105 
106 theorem finiteSum_le_norm (x : Q.Space) (c : Coefficients 𝕜) :
107     ‖finiteSum x.val c‖ ≤ Q.unconditionalNorm x :=
108   le_csSup (Q.signedValues_bddAbove x) ⟨c, rfl⟩
109 
110 theorem coordinate_le_norm (x : Q.Space) (n : ℕ) : ‖x.val n‖ ≤ Q.unconditionalNorm x := by
111   simpa [finiteSum] using
112     Q.finiteSum_le_norm x (⟨{n}, ⟨fun _ ↦ 1, by simp⟩⟩ : Coefficients 𝕜)
113 
114 theorem unconditionalNorm_add_le (x y : Q.Space) :
115     Q.unconditionalNorm (x + y) ≤ Q.unconditionalNorm x + Q.unconditionalNorm y := by
116   apply csSup_le (Q.signedValues_nonempty (x + y))
117   rintro v ⟨c, rfl⟩
118   change ‖∑ n ∈ c.1, c.2.val n • (x.val n + y.val n)‖ ≤ _
119   simp_rw [smul_add, Finset.sum_add_distrib]
120   exact (norm_add_le _ _).trans
121     (add_le_add (Q.finiteSum_le_norm x c) (Q.finiteSum_le_norm y c))
122 
123 theorem unconditionalNorm_neg (x : Q.Space) :
124     Q.unconditionalNorm (-x) = Q.unconditionalNorm x := by
125   have h : Q.signedValues (-x) = Q.signedValues x := by
126     ext v
127     simp [signedValues, finiteSum, smul_neg, Finset.sum_neg_distrib, norm_neg]
128   exact congrArg sSup h
129 
130 theorem unconditionalNorm_zero : Q.unconditionalNorm 0 = 0 := by
131   apply le_antisymm
132   · apply csSup_le (Q.signedValues_nonempty 0)
133     rintro v ⟨c, rfl⟩
134     simp [finiteSum]
135   · simpa using Q.coordinate_le_norm 0 0
136 
137 theorem eq_zero_of_unconditionalNorm_eq_zero (x : Q.Space)
138     (hx : Q.unconditionalNorm x = 0) : x = 0 := by
139   ext n
140   apply norm_eq_zero.mp
141   exact le_antisymm (hx ▸ Q.coordinate_le_norm x n) (norm_nonneg _)
142 
143 def spaceNorm : AddGroupNorm Q.Space where
144   toFun := Q.unconditionalNorm
145   map_zero' := Q.unconditionalNorm_zero
146   add_le' := Q.unconditionalNorm_add_le
147   neg' := Q.unconditionalNorm_neg
148   eq_zero_of_map_eq_zero' := Q.eq_zero_of_unconditionalNorm_eq_zero
149 
150 instance spaceNormedAddCommGroup : NormedAddCommGroup Q.Space :=
151   Q.spaceNorm.toNormedAddCommGroup
152 
153 @[simp] theorem space_norm_eq (x : Q.Space) : ‖x‖ = Q.unconditionalNorm x := rfl
154 
155 instance spaceNormedSpace : NormedSpace 𝕜 Q.Space where
156   norm_smul_le a x := by
157     change Q.unconditionalNorm (a • x) ≤ ‖a‖ * Q.unconditionalNorm x
158     apply csSup_le (Q.signedValues_nonempty (a • x))
159     rintro v ⟨c, rfl⟩
160     change ‖∑ n ∈ c.1, c.2.val n • (a • x.val n)‖ ≤ _
161     have he : (∑ n ∈ c.1, c.2.val n • (a • x.val n)) =
162         a • (∑ n ∈ c.1, c.2.val n • x.val n) := by
163       simp only [Finset.smul_sum, smul_smul]
164       congr 1
165       ext n
166       rw [mul_comm]
167     rw [he, norm_smul]
168     exact mul_le_mul_of_nonneg_left (Q.finiteSum_le_norm x c) (norm_nonneg a)
169 
170 theorem coordinate_dist_le (x y : Q.Space) (n : ℕ) :
171     dist (x.val n) (y.val n) ≤ dist x y := by
172   simpa only [dist_eq_norm, space_sub_val, space_norm_eq] using Q.coordinate_le_norm (x - y) n
173 
174 /-- A Cauchy sequence in the signed-sum norm is Cauchy in every coordinate. -/
175 theorem coordinate_cauchy (u : ℕ → Q.Space) (hu : CauchySeq u) (n : ℕ) :
176     CauchySeq (fun k ↦ (u k).val n) := by
177   apply Metric.cauchySeq_iff.mpr
178   intro ε hε
179   obtain ⟨N, hN⟩ := Metric.cauchySeq_iff.mp hu ε hε
180   exact ⟨N, fun i hi j hj ↦ (Q.coordinate_dist_le (u i) (u j) n).trans_lt (hN i hi j hj)⟩
181 
182 /-- Every finite multiplier estimate passes to a coordinatewise limit.
183 The same Cauchy index works for all finite subsets and coefficients. -/
184 theorem finiteSum_limit_bound (u : ℕ → Q.Space) (y : ℕ → X)
185     (hy : ∀ n, Tendsto (fun k ↦ (u k).val n) atTop (𝓝 (y n)))
186     (N m : ℕ) (ε : ℝ) (hN : ∀ k ≥ N, ‖u k - u m‖ < ε)
187     (c : Coefficients 𝕜) :
188     ‖finiteSum (fun n ↦ y n - (u m).val n) c‖ ≤ ε := by
189   have hlim : Tendsto (fun k ↦ finiteSum (u k - u m).val c) atTop
190       (𝓝 (finiteSum (fun n ↦ y n - (u m).val n) c)) := by
191     apply tendsto_finsetSum
192     intro n _
193     exact ((hy n).sub tendsto_const_nhds).const_smul (c.2.val n)
194   apply le_of_tendsto hlim.norm
195   filter_upwards [eventually_ge_atTop N] with k hk
196   exact (Q.finiteSum_le_norm (u k - u m) c).trans (hN k hk).le
197 
198 /-- Coordinate limits of a signed-norm Cauchy sequence approximate all
199 finite multiplier sums uniformly. -/
200 theorem finiteSum_uniform_limit (u : ℕ → Q.Space) (hu : CauchySeq u) (y : ℕ → X)
201     (hy : ∀ n, Tendsto (fun k ↦ (u k).val n) atTop (𝓝 (y n))) :
202     ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ c : Coefficients 𝕜,
203       ‖finiteSum (fun n ↦ y n - (u m).val n) c‖ ≤ ε := by
204   intro ε hε
205   obtain ⟨N, hN⟩ := Metric.cauchySeq_iff.mp hu ε hε
206   refine ⟨N, fun m hm c ↦ Q.finiteSum_limit_bound u y hy N m ε ?_ c⟩
207   intro k hk
208   simpa only [dist_eq_norm] using hN k hk m hm
209 
210 /-- The coordinate limit is still unconditionally summable. -/
211 theorem summable_coordinate_limit [CompleteSpace X]
212     (u : ℕ → Q.Space) (hu : CauchySeq u) (y : ℕ → X)
213     (hy : ∀ n, Tendsto (fun k ↦ (u k).val n) atTop (𝓝 (y n))) : Summable y := by
214   apply summable_iff_vanishing_norm.mpr
215   intro ε hε
216   obtain ⟨N, hN⟩ := Q.finiteSum_uniform_limit u hu y hy (ε / 2) (half_pos hε)
217   obtain ⟨F, hF⟩ := summable_iff_vanishing_norm.mp (u N).property.2
218     (ε / 2) (half_pos hε)
219   refine ⟨F, fun G hG ↦ ?_⟩
220   have hdiff : ‖∑ n ∈ G, (y n - (u N).val n)‖ ≤ ε / 2 := by
221     simpa [finiteSum] using hN N le_rfl (⟨G, ⟨fun _ ↦ 1, by simp⟩⟩ : Coefficients 𝕜)
222   have he : (∑ n ∈ G, y n) =
223       (∑ n ∈ G, (y n - (u N).val n)) + (∑ n ∈ G, (u N).val n) := by
224     rw [Finset.sum_sub_distrib]
225     exact (sub_add_cancel _ _).symm
226   rw [he]
227   exact (norm_add_le _ _).trans_lt
228     ((add_lt_add_of_le_of_lt hdiff (hF G hG)).trans_eq (add_halves ε))
229 
230 /-- The literal unconditional sum space of arbitrary closed subspaces of
231 a real or complex Banach space is complete. -/
232 instance spaceCompleteSpace [CompleteSpace X] : CompleteSpace Q.Space := by
233   apply Metric.complete_of_cauchySeq_tendsto
234   intro u hu
235   have hcoord : ∀ n, ∃ y : X, Tendsto (fun k ↦ (u k).val n) atTop (𝓝 y) :=
236     fun n ↦ cauchySeq_tendsto_of_complete (Q.coordinate_cauchy u hu n)
237   choose y hy using hcoord
238   have hmem : ∀ n, y n ∈ Q.packet n := by
239     intro n
240     exact (Q.closed n).mem_of_tendsto (hy n) (Eventually.of_forall fun k ↦ (u k).property.1 n)
241   let z : Q.Space := ⟨y, hmem, Q.summable_coordinate_limit u hu y hy⟩
242   refine ⟨z, Metric.tendsto_atTop.mpr ?_⟩
243   intro ε hε
244   obtain ⟨N, hN⟩ := Q.finiteSum_uniform_limit u hu y hy (ε / 2) (half_pos hε)
245   refine ⟨N, fun m hm ↦ ?_⟩
246   rw [dist_comm, dist_eq_norm, space_norm_eq]
247   have hnorm : Q.unconditionalNorm (z - u m) ≤ ε / 2 := by
248     apply csSup_le (Q.signedValues_nonempty (z - u m))
249     rintro v ⟨c, rfl⟩
250     exact hN m hm c
251   exact hnorm.trans_lt (half_lt_self hε)
252 
253 end ClosedPackets
254 
255 end PaperIRelease.TopologyUnconditional

Back to source controls