BanachBlocks.lean

1 import KomorebiSpace.BanachTowers
2 import KomorebiSpace.AdjacentResolution
3 import Mathlib.Algebra.BigOperators.Intervals
4 import Mathlib.Tactic.Abel
5 import Mathlib.Tactic.Ring
6 
7 set_option autoImplicit false
8 
9 /-!
10 # Actual block restrictions and accumulated tower residuals
11 
12 All maps below use the existing Banach tower bonding maps. A block residual is
13 not a subsample of adjacent residuals: it is their transported accumulation.
14 Contractivity is an explicit extra hypothesis for the norm estimates.
15 -/
16 
17 universe u v
18 noncomputable section
19 namespace KomorebiSpace
20 namespace BanachTower
21 open scoped NNReal ENNReal
22 variable {𝕜 : Type u} [NontriviallyNormedField 𝕜]
23 variable (X Y : BanachTower.{u,v} 𝕜)
24 
25 /-- The actual continuous linear restriction between any ordered pair of stages. -/
26 def restriction {i j : ℕ} (h : i ≤ j) : X.Obj j →L[𝕜] X.Obj i :=
27   Nat.leRecOn (C := fun n => X.Obj n →L[𝕜] X.Obj i) h
28     (fun {n} a => a.comp (X.down n)) (ContinuousLinearMap.id 𝕜 (X.Obj i))
29 
30 @[simp] theorem restriction_refl (i : ℕ) :
31     restriction X (Nat.le_refl i) = ContinuousLinearMap.id 𝕜 (X.Obj i) := by
32   simp [restriction, Nat.leRecOn_self]
33 
34 theorem restriction_succ {i j : ℕ} (h : i ≤ j) (h' : i ≤ j+1) :
35     restriction X h' = (restriction X h).comp (X.down j) := by
36   simp only [restriction, Nat.leRecOn_succ h]
37 
38 @[simp] theorem restriction_adjacent (i : ℕ) :
39     restriction X (Nat.le_succ i) = X.down i := by
40   rw [restriction_succ X (Nat.le_refl i), restriction_refl]
41   ext x
42   rfl
43 
44 theorem restriction_trans {i j k : ℕ} (hij : i ≤ j) (hjk : j ≤ k) :
45     (restriction X hij).comp (restriction X hjk) =
46       restriction X (hij.trans hjk) := by
47   induction k, hjk using Nat.le_induction with
48   | base => simp
49   | succ k hk ih =>
50     rw [restriction_succ X hk, restriction_succ X (hij.trans hk)]
51     rw [← ContinuousLinearMap.comp_assoc, ih]
52 
53 /-- Agreement with the finite-stage functions in the previous eventual category. -/
54 theorem restriction_underlying {i j : ℕ} (h : i ≤ j) (x : X.Obj j) :
55     restriction X h x = (Resolution.Adjacent.resolution X.Obj (fun n => X.down n)).restrict h x := by
56   induction j, h using Nat.le_induction with
57   | base => simp [Resolution.Adjacent.resolution]
58   | succ j hj ih =>
59     rw [restriction_succ X hj]
60     change restriction X hj (X.down j x) =
61       Resolution.Adjacent.restrict X.Obj (fun n => X.down n) _ x
62     rw [Resolution.Adjacent.restrict_succ X.Obj (fun n => X.down n) hj]
63     exact ih (X.down j x)
64 
65 /-- All-pairs restrictions are contractive when adjacent bonds are. -/
66 theorem restriction_contractive (hX : ∀ n, ‖X.down n‖ ≤ 1)
67     {i j : ℕ} (h : i ≤ j) : ‖restriction X h‖ ≤ 1 := by
68   induction j, h using Nat.le_induction with
69   | base => simpa using (ContinuousLinearMap.norm_id_le (𝕜 := 𝕜) (E := X.Obj i))
70   | succ j hj ih =>
71     rw [restriction_succ X hj]
72     exact ((restriction X hj).opNorm_comp_le (X.down j)).trans
73       ((mul_le_mul ih (hX j) (norm_nonneg _) (by norm_num)).trans (by norm_num))
74 
75 /-- Noncommuting comparison for an entire block. -/
76 def blockDefect (f : Candidates X Y) {i j : ℕ} (h : i ≤ j) :
77     X.Obj j →L[𝕜] Y.Obj i :=
78   (restriction Y h).comp (f j) - (f i).comp (restriction X h)
79 
80 @[simp] theorem blockDefect_refl (f : Candidates X Y) (i : ℕ) :
81     blockDefect X Y f (Nat.le_refl i) = 0 := by
82   ext x
83   simp [blockDefect]
84 
85 @[simp] theorem blockDefect_adjacent (f : Candidates X Y) (i : ℕ) :
86     blockDefect X Y f (Nat.le_succ i) = rawDefect X Y f i := by
87   simp [blockDefect, rawDefect]
88 
89 /-- Exact concatenation law, with the two defects in the correct common Hom space. -/
90 theorem blockDefect_concat (f : Candidates X Y) {i j k : ℕ}
91     (hij : i ≤ j) (hjk : j ≤ k) :
92     blockDefect X Y f (hij.trans hjk) =
93       (restriction Y hij).comp (blockDefect X Y f hjk) +
94       (blockDefect X Y f hij).comp (restriction X hjk) := by
95   unfold blockDefect
96   rw [← restriction_trans X hij hjk, ← restriction_trans Y hij hjk]
97   ext x
98   simp only [ContinuousLinearMap.comp_apply, sub_apply,
99     add_apply, map_sub]
100   abel
101 
102 theorem blockDefect_succ (f : Candidates X Y) {i j : ℕ} (h : i ≤ j) :
103     blockDefect X Y f (h.trans (Nat.le_succ j)) =
104       (restriction Y h).comp (rawDefect X Y f j) +
105       (blockDefect X Y f h).comp (X.down j) := by
106   rw [blockDefect_concat X Y f h (Nat.le_succ j)]
107   simp
108 
109 /-- Transported accumulation of any family of adjacent residuals. -/
110 def blockSum (r : ∀ n, X.Obj (n+1) →L[𝕜] Y.Obj n) {i j : ℕ} (h : i ≤ j) :
111     X.Obj j →L[𝕜] Y.Obj i :=
112   Nat.leRecOn (C := fun n => X.Obj n →L[𝕜] Y.Obj i) h
113     (fun {n} a => if hn : i ≤ n then
114       (restriction Y hn).comp (r n) + a.comp (X.down n) else 0) 0
115 
116 @[simp] theorem blockSum_refl (r : ∀ n, X.Obj (n+1) →L[𝕜] Y.Obj n) (i : ℕ) :
117     blockSum X Y r (Nat.le_refl i) = 0 := by
118   simp [blockSum, Nat.leRecOn_self]
119 
120 theorem blockSum_succ (r : ∀ n, X.Obj (n+1) →L[𝕜] Y.Obj n)
121     {i j : ℕ} (h : i ≤ j) (h' : i ≤ j+1) :
122     blockSum X Y r h' =
123       (restriction Y h).comp (r j) + (blockSum X Y r h).comp (X.down j) := by
124   simp only [blockSum, Nat.leRecOn_succ h, dite_eq_left h]
125 
126 @[simp] theorem blockSum_adjacent (r : ∀ n, X.Obj (n+1) →L[𝕜] Y.Obj n) (i : ℕ) :
127     blockSum X Y r (Nat.le_succ i) = r i := by
128   rw [blockSum_succ X Y r (Nat.le_refl i)]
129   simp
130 
131 /-- Fundamental telescoping identity, on the actual tower differential. -/
132 theorem blockSum_differential (f : Candidates X Y) {i j : ℕ} (h : i ≤ j) :
133     blockSum X Y (differential X Y f) h = blockDefect X Y f h := by
134   induction j, h using Nat.le_induction with
135   | base => simp
136   | succ j hj ih =>
137     rw [blockSum_succ X Y _ hj, blockDefect_succ, ih]
138     rfl
139 
140 theorem blockSum_add (r s : ∀ n, X.Obj (n+1) →L[𝕜] Y.Obj n)
141     {i j : ℕ} (h : i ≤ j) :
142     blockSum X Y (r+s) h = blockSum X Y r h + blockSum X Y s h := by
143   induction j, h using Nat.le_induction with
144   | base => simp
145   | succ j hj ih =>
146     rw [blockSum_succ X Y _ hj, blockSum_succ X Y r hj,
147       blockSum_succ X Y s hj, ih]
148     ext x
149     simp only [Pi.add_apply, ContinuousLinearMap.comp_apply,
150       add_apply, map_add]
151     abel
152 
153 theorem blockSum_smul (c : 𝕜) (r : ∀ n, X.Obj (n+1) →L[𝕜] Y.Obj n)
154     {i j : ℕ} (h : i ≤ j) :
155     blockSum X Y (c • r) h = c • blockSum X Y r h := by
156   induction j, h using Nat.le_induction with
157   | base => simp
158   | succ j hj ih =>
159     rw [blockSum_succ X Y _ hj, blockSum_succ X Y r hj, ih]
160     ext x
161     simp [smul_add]
162 
163 /-- A local sum budget, without cancellation being discarded from the residual itself. -/
164 theorem blockSum_norm (hX : ∀ n, ‖X.down n‖ ≤ 1) (hY : ∀ n, ‖Y.down n‖ ≤ 1)
165     (r : ∀ n, X.Obj (n+1) →L[𝕜] Y.Obj n) {i j : ℕ} (h : i ≤ j) :
166     ‖blockSum X Y r h‖ ≤ ∑ k ∈ Finset.Ico i j, ‖r k‖ := by
167   induction j, h using Nat.le_induction with
168   | base => simp
169   | succ j hj ih =>
170     rw [blockSum_succ X Y r hj, Finset.sum_Ico_succ_top hj]
171     have h1 : ‖(restriction Y hj).comp (r j)‖ ≤ ‖r j‖ :=
172       ((restriction Y hj).opNorm_comp_le (r j)).trans
173         (by simpa using (mul_le_mul_of_nonneg_right (restriction_contractive Y hY hj)
174           (norm_nonneg (r j))))
175     have h2 : ‖(blockSum X Y r hj).comp (X.down j)‖ ≤ ‖blockSum X Y r hj‖ :=
176       ((blockSum X Y r hj).opNorm_comp_le (X.down j)).trans
177         (by simpa using (mul_le_mul_of_nonneg_left (hX j) (norm_nonneg (blockSum X Y r hj))))
178     exact (norm_add_le _ _).trans ((add_le_add h1 (h2.trans ih)).trans (by rw [add_comm]))
179 
180 theorem blockSum_uniform_bound (hX : ∀ n, ‖X.down n‖ ≤ 1)
181     (hY : ∀ n, ‖Y.down n‖ ≤ 1) (r : Residuals X Y) {i j : ℕ} (h : i ≤ j) :
182     ‖blockSum X Y r h‖ ≤ (j-i : ℕ) * ‖r‖ := by
183   apply (blockSum_norm X Y hX hY r h).trans
184   calc
185     (∑ k ∈ Finset.Ico i j, ‖r k‖) ≤ ∑ _k ∈ Finset.Ico i j, ‖r‖ :=
186       Finset.sum_le_sum (fun k _ => lp.norm_apply_le_norm ENNReal.top_ne_zero r k)
187     _ = (j-i : ℕ) * ‖r‖ := by simp
188 
189 theorem blockDefect_uniform_bound (hX : ∀ n, ‖X.down n‖ ≤ 1)
190     (hY : ∀ n, ‖Y.down n‖ ≤ 1) (f : Candidates X Y) {i j : ℕ} (h : i ≤ j) :
191     ‖blockDefect X Y f h‖ ≤ (j-i : ℕ) * ‖differential X Y f‖ := by
192   rw [← blockSum_differential X Y f h]
193   exact blockSum_uniform_bound X Y hX hY _ h
194 
195 end BanachTower
196 end KomorebiSpace
197 end

Back to source controls