TopologyCountablePackets.lean

1 import KomorebiVerification.TopologicalCompletion
2 import Mathlib.Analysis.Normed.Group.Seminorm
3 
4 /-! # Unconditional countable packet coordinates
5 
6 The carrier is the literal space of unconditionally summable packet
7 sequences. Its norm is the supremum over finite coefficient-weighted sums.
8 -/
9 
10 noncomputable section
11 open scoped BigOperators
12 open Set Function Filter
13 
14 namespace PaperIRelease.TopologyCountablePackets
15 
16 variable {𝕜 X : Type*} [NontriviallyNormedField 𝕜]
17 variable [NormedAddCommGroup X] [NormedSpace 𝕜 X]
18 
19 /-- Countably many mutually annihilating bounded projections with
20 unconditional reconstruction and an explicit uniform multiplier bound. -/
21 structure Projectors (𝕜 X : Type*) [NontriviallyNormedField 𝕜]
22     [NormedAddCommGroup X] [NormedSpace 𝕜 X] where
23   proj : ℕ → X →L[𝕜] X
24   idempotent : ∀ i x, proj i (proj i x) = proj i x
25   annihilate : ∀ {i j}, i ≠ j → ∀ x, proj i (proj j x) = 0
26   complete : ∀ x, HasSum (fun i ↦ proj i x) x
27   K : ℝ
28   nonneg_K : 0 ≤ K
29   bound : ∀ (F : Finset ℕ) (a : ℕ → 𝕜), (∀ n, ‖a n‖ ≤ 1) →
30     ‖∑ n ∈ F, a n • proj n‖ ≤ K
31 
32 namespace Projectors
33 
34 /-- The operator norms whose supremum is the manuscript constant `K`. -/
35 def multiplierNorms (P : ℕ → X →L[𝕜] X) : Set ℝ :=
36   {v | ∃ F : Finset ℕ, ∃ a : ℕ → 𝕜, (∀ n, ‖a n‖ ≤ 1) ∧
37     v = ‖∑ n ∈ F, a n • P n‖}
38 
39 /-- Construct the packet theorem's data using the exact supremum constant,
40 from the manuscript's boundedness hypothesis on finite multiplier sums. -/
41 def ofSupBound (P : ℕ → X →L[𝕜] X)
42     (hid : ∀ i x, P i (P i x) = P i x)
43     (hann : ∀ {i j}, i ≠ j → ∀ x, P i (P j x) = 0)
44     (hsum : ∀ x, HasSum (fun i ↦ P i x) x)
45     (hbound : BddAbove (multiplierNorms P)) : Projectors 𝕜 X where
46   proj := P
47   idempotent := hid
48   annihilate := hann
49   complete := hsum
50   K := sSup (multiplierNorms P)
51   nonneg_K := le_csSup hbound ⟨∅, fun _ ↦ 0, by simp, by simp⟩
52   bound F a ha := le_csSup hbound ⟨F, a, ha, rfl⟩
53 
54 variable (P : Projectors 𝕜 X)
55 
56 /-- Exactly the sequences in the packet ranges whose series converges
57 unconditionally. `Summable` uses the net over all finite subsets. -/
58 def packetSequences : Submodule 𝕜 (ℕ → X) where
59   carrier := {x | (∀ n, x n ∈ (P.proj n).range) ∧ Summable x}
60   zero_mem' := ⟨fun _ ↦ Submodule.zero_mem _, summable_zero⟩
61   add_mem' := by
62     rintro x y ⟨hx, hxs⟩ ⟨hy, hys⟩
63     exact ⟨fun n ↦ Submodule.add_mem _ (hx n) (hy n), hxs.add hys⟩
64   smul_mem' := by
65     rintro c x ⟨hx, hxs⟩
66     exact ⟨fun n ↦ Submodule.smul_mem _ c (hx n), hxs.const_smul c⟩
67 
68 /-- The packet carrier as a type with the signed-sum norm, rather than
69 the unrelated product topology on all sequences. -/
70 def PacketSpace : Type _ := P.packetSequences
71 
72 instance packetAddCommGroup : AddCommGroup P.PacketSpace :=
73   inferInstanceAs (AddCommGroup P.packetSequences)
74 
75 instance packetModule : Module 𝕜 P.PacketSpace :=
76   inferInstanceAs (Module 𝕜 P.packetSequences)
77 
78 @[ext]
79 theorem PacketSpace.ext (x y : P.PacketSpace) (h : ∀ n, x.val n = y.val n) : x = y :=
80   Subtype.ext (funext h)
81 
82 @[simp]
83 theorem packet_neg_val (x : P.PacketSpace) (n : ℕ) : (-x).val n = -x.val n := rfl
84 
85 /-- Analysis takes the actual projector coordinates. -/
86 def analysis : X →ₗ[𝕜] P.PacketSpace where
87   toFun x := ⟨fun n ↦ P.proj n x, ⟨fun n ↦ ⟨x, rfl⟩, (P.complete x).summable⟩⟩
88   map_add' _ _ := by ext n; exact map_add _ _ _
89   map_smul' _ _ := by ext n; exact map_smul _ _ _
90 
91 /-- Synthesis is the unconditional sum in the original ambient space. -/
92 def synthesis : P.PacketSpace →ₗ[𝕜] X where
93   toFun x := ∑' n, x.val n
94   map_add' x y := x.property.2.tsum_add y.property.2
95   map_smul' c x := x.property.2.tsum_const_smul c
96 
97 @[simp]
98 theorem synthesis_analysis (x : X) : P.synthesis (P.analysis x) = x :=
99   (P.complete x).tsum_eq
100 
101 @[simp]
102 theorem analysis_synthesis (x : P.PacketSpace) : P.analysis (P.synthesis x) = x := by
103   ext n
104   change P.proj n (∑' j, x.val j) = x.val n
105   rw [(P.proj n).map_tsum x.property.2]
106   rw [tsum_eq_single n]
107   · obtain ⟨y, hy⟩ := x.property.1 n
108     rw [← hy]
109     exact P.idempotent n y
110   · intro j hj
111     obtain ⟨y, hy⟩ := x.property.1 j
112     rw [← hy]
113     exact P.annihilate hj.symm y
114 
115 /-- Algebraic analysis and synthesis are inverse on the literal
116 unconditionally summable packet carrier. -/
117 def packetLinearEquiv : X ≃ₗ[𝕜] P.PacketSpace :=
118   LinearEquiv.ofLinearMap P.analysis P.synthesis
119     (LinearMap.ext P.analysis_synthesis) (LinearMap.ext P.synthesis_analysis)
120 
121 /-- All finite coefficient-weighted sum norms from the printed definition. -/
122 def signedValues (x : P.PacketSpace) : Set ℝ :=
123   {v | ∃ F : Finset ℕ, ∃ a : ℕ → 𝕜, (∀ n, ‖a n‖ ≤ 1) ∧
124     v = ‖∑ n ∈ F, a n • x.val n‖}
125 
126 theorem signedValues_nonempty (x : P.PacketSpace) : (P.signedValues x).Nonempty :=
127   ⟨0, ∅, fun _ ↦ 0, by simp, by simp⟩
128 
129 theorem signed_sum_le (x : P.PacketSpace) (F : Finset ℕ) (a : ℕ → 𝕜)
130     (ha : ∀ n, ‖a n‖ ≤ 1) :
131     ‖∑ n ∈ F, a n • x.val n‖ ≤ P.K * ‖P.synthesis x‖ := by
132   have hx : ∀ n, P.proj n (P.synthesis x) = x.val n := by
133     intro n
134     exact congrArg (fun z : P.PacketSpace ↦ z.val n) (P.analysis_synthesis x)
135   calc
136     ‖∑ n ∈ F, a n • x.val n‖ = ‖(∑ n ∈ F, a n • P.proj n) (P.synthesis x)‖ := by
137       simp only [sum_apply, smul_apply, hx]
138     _ ≤ ‖∑ n ∈ F, a n • P.proj n‖ * ‖P.synthesis x‖ :=
139       ContinuousLinearMap.le_opNorm _ _
140     _ ≤ P.K * ‖P.synthesis x‖ := mul_le_mul_of_nonneg_right (P.bound F a ha) (norm_nonneg _)
141 
142 theorem signedValues_bddAbove (x : P.PacketSpace) : BddAbove (P.signedValues x) := by
143   refine ⟨P.K * ‖P.synthesis x‖, ?_⟩
144   rintro v ⟨F, a, ha, rfl⟩
145   exact P.signed_sum_le x F a ha
146 
147 /-- The literal unconditional signed-sum norm. -/
148 def unconditionalNorm (x : P.PacketSpace) : ℝ := sSup (P.signedValues x)
149 
150 theorem signed_sum_le_norm (x : P.PacketSpace) (F : Finset ℕ) (a : ℕ → 𝕜)
151     (ha : ∀ n, ‖a n‖ ≤ 1) :
152     ‖∑ n ∈ F, a n • x.val n‖ ≤ P.unconditionalNorm x :=
153   le_csSup (P.signedValues_bddAbove x) ⟨F, a, ha, rfl⟩
154 
155 theorem norm_le_K_synthesis (x : P.PacketSpace) :
156     P.unconditionalNorm x ≤ P.K * ‖P.synthesis x‖ := by
157   apply csSup_le (P.signedValues_nonempty x)
158   rintro v ⟨F, a, ha, rfl⟩
159   exact P.signed_sum_le x F a ha
160 
161 theorem synthesis_norm_le (x : P.PacketSpace) : ‖P.synthesis x‖ ≤ P.unconditionalNorm x := by
162   apply le_of_tendsto x.property.2.hasSum.norm
163   apply Eventually.of_forall
164   intro F
165   simpa using P.signed_sum_le_norm x F (fun _ ↦ 1) (by simp)
166 
167 theorem unconditionalNorm_add_le (x y : P.PacketSpace) :
168     P.unconditionalNorm (x + y) ≤ P.unconditionalNorm x + P.unconditionalNorm y := by
169   apply csSup_le (P.signedValues_nonempty (x + y))
170   rintro v ⟨F, a, ha, rfl⟩
171   change ‖∑ n ∈ F, a n • (x.val n + y.val n)‖ ≤ _
172   simp_rw [smul_add, Finset.sum_add_distrib]
173   exact (norm_add_le _ _).trans
174     (add_le_add (P.signed_sum_le_norm x F a ha) (P.signed_sum_le_norm y F a ha))
175 
176 theorem unconditionalNorm_neg (x : P.PacketSpace) :
177     P.unconditionalNorm (-x) = P.unconditionalNorm x := by
178   have h : P.signedValues (-x) = P.signedValues x := by
179     ext v
180     simp [signedValues, smul_neg,
181       Finset.sum_neg_distrib, norm_neg]
182   exact congrArg sSup h
183 
184 theorem unconditionalNorm_zero : P.unconditionalNorm 0 = 0 := by
185   apply le_antisymm
186   · simpa using P.norm_le_K_synthesis 0
187   · simpa using P.synthesis_norm_le 0
188 
189 theorem eq_zero_of_unconditionalNorm_eq_zero (x : P.PacketSpace)
190     (hx : P.unconditionalNorm x = 0) : x = 0 := by
191   have hs : P.synthesis x = 0 := by
192     apply norm_eq_zero.mp
193     exact le_antisymm (hx ▸ P.synthesis_norm_le x) (norm_nonneg _)
194   rw [← P.analysis_synthesis x, hs, map_zero]
195 
196 /-- The signed-sum supremum is a norm on the full packet sequence carrier. -/
197 def packetNorm : AddGroupNorm P.PacketSpace where
198   toFun := P.unconditionalNorm
199   map_zero' := P.unconditionalNorm_zero
200   add_le' := P.unconditionalNorm_add_le
201   neg' := P.unconditionalNorm_neg
202   eq_zero_of_map_eq_zero' := P.eq_zero_of_unconditionalNorm_eq_zero
203 
204 instance packetNormedAddCommGroup : NormedAddCommGroup P.PacketSpace :=
205   P.packetNorm.toNormedAddCommGroup
206 
207 @[simp]
208 theorem packet_norm_eq (x : P.PacketSpace) : ‖x‖ = P.unconditionalNorm x := rfl
209 
210 instance packetNormedSpace : NormedSpace 𝕜 P.PacketSpace where
211   norm_smul_le c x := by
212     change P.unconditionalNorm (c • x) ≤ ‖c‖ * P.unconditionalNorm x
213     apply csSup_le (P.signedValues_nonempty (c • x))
214     rintro v ⟨F, a, ha, rfl⟩
215     change ‖∑ n ∈ F, a n • (c • x.val n)‖ ≤ _
216     have he : (∑ n ∈ F, a n • (c • x.val n)) =
217         c • (∑ n ∈ F, a n • x.val n) := by
218       simp only [Finset.smul_sum, smul_smul]
219       congr 1
220       ext n
221       rw [mul_comm]
222     rw [he, norm_smul]
223     exact mul_le_mul_of_nonneg_left (P.signed_sum_le_norm x F a ha) (norm_nonneg c)
224 
225 /-- Analysis and synthesis are inverse bounded linear maps for the exact
226 unconditional signed-sum norm. -/
227 def packetEquiv : X ≃L[𝕜] P.PacketSpace :=
228   P.packetLinearEquiv.toContinuousLinearEquivOfBounds P.K 1
229     (fun x ↦ by simpa [packetLinearEquiv] using P.norm_le_K_synthesis (P.analysis x))
230     (fun x ↦ by simpa [packetLinearEquiv] using P.synthesis_norm_le x)
231 
232 @[simp]
233 theorem packetEquiv_apply (x : X) : P.packetEquiv x = P.analysis x := rfl
234 
235 @[simp]
236 theorem packetEquiv_symm_apply (x : P.PacketSpace) : P.packetEquiv.symm x = P.synthesis x := rfl
237 
238 /-- Completeness of the countable packet space follows from its constructed
239 uniform equivalence with the Banach ambient space. -/
240 instance packetCompleteSpace [CompleteSpace X] : CompleteSpace P.PacketSpace :=
241   (P.packetEquiv.isUniformEmbedding.isUniformInducing.completeSpace_congr
242     P.packetEquiv.surjective).mp inferInstance
243 
244 /-- Quantitative analysis bound from the stated uniform multiplier bound. -/
245 theorem analysis_opNorm_le : ‖P.packetEquiv.toContinuousLinearMap‖ ≤ P.K := by
246   apply ContinuousLinearMap.opNorm_le_bound _ P.nonneg_K
247   intro x
248   change P.unconditionalNorm (P.analysis x) ≤ P.K * ‖x‖
249   simpa using P.norm_le_K_synthesis (P.analysis x)
250 
251 /-- Quantitative synthesis bound, with constant exactly one. -/
252 theorem synthesis_opNorm_le : ‖P.packetEquiv.symm.toContinuousLinearMap‖ ≤ 1 := by
253   apply ContinuousLinearMap.opNorm_le_bound _ zero_le_one
254   intro x
255   change ‖P.synthesis x‖ ≤ 1 * P.unconditionalNorm x
256   simpa using P.synthesis_norm_le x
257 
258 end Projectors
259 
260 end PaperIRelease.TopologyCountablePackets

Back to source controls