GrowingTower.lean

1 import KomorebiSpace.SplitTowerCoordinates
2 import Mathlib.Data.Fin.Tuple.Basic
3 
4 set_option autoImplicit false
5 
6 /-!
7 # An explicit, dimension-growing tower model
8 
9 Stage n is real coordinate space of dimension n+1 with its sup norm.
10 The source coarse-graining is half the coordinate truncation; the target
11 coarse-graining is unscaled truncation. Zero extension supplies the target
12 splitting. Every hypothesis of the split-tower repair theorem is verified.
13 -/
14 noncomputable section
15 open scoped NNReal ENNReal
16 namespace KomorebiSpace
17 namespace GrowingTower
18 open BanachTower
19 
20 abbrev Stage (n : ℕ) := Fin (n+1) → ℝ
21 
22 def dropLinear (n : ℕ) : Stage (n+1) →ₗ[ℝ] Stage n where
23   toFun x i := x i.castSucc
24   map_add' _ _ := rfl
25   map_smul' _ _ := rfl
26 
27 theorem dropLinear_bound (n : ℕ) (x : Stage (n+1)) : ‖dropLinear n x‖ ≤ ‖x‖ := by
28   apply (pi_norm_le_iff_of_nonneg (norm_nonneg x)).mpr
29   intro i
30   exact norm_le_pi_norm x i.castSucc
31 
32 def drop (n : ℕ) : Stage (n+1) →L[ℝ] Stage n :=
33   (dropLinear n).mkContinuous 1 (fun x => by simpa using dropLinear_bound n x)
34 
35 @[simp] theorem drop_apply (n : ℕ) (x : Stage (n+1)) (i : Fin (n+1)) :
36     drop n x i = x i.castSucc := rfl
37 
38 theorem drop_opNorm (n : ℕ) : ‖drop n‖ ≤ 1 :=
39   ContinuousLinearMap.opNorm_le_bound _ zero_le_one
40     (fun x => by simpa only [drop, LinearMap.mkContinuous_apply, one_mul] using dropLinear_bound n x)
41 
42 def insertLinear (n : ℕ) : Stage n →ₗ[ℝ] Stage (n+1) where
43   toFun x := Fin.snoc x 0
44   map_add' x y := by
45     funext i
46     refine Fin.lastCases ?_ (fun j => ?_) i <;> simp
47   map_smul' c x := by
48     funext i
49     refine Fin.lastCases ?_ (fun j => ?_) i <;> simp
50 
51 theorem insertLinear_bound (n : ℕ) (x : Stage n) : ‖insertLinear n x‖ ≤ ‖x‖ := by
52   apply (pi_norm_le_iff_of_nonneg (norm_nonneg x)).mpr
53   intro i
54   refine Fin.lastCases ?_ (fun j => ?_) i
55   · simp [insertLinear]
56   · simpa [insertLinear] using norm_le_pi_norm x j
57 
58 def insert (n : ℕ) : Stage n →L[ℝ] Stage (n+1) :=
59   (insertLinear n).mkContinuous 1 (fun x => by simpa using insertLinear_bound n x)
60 
61 @[simp] theorem insert_old (n : ℕ) (x : Stage n) (i : Fin (n+1)) :
62     insert n x i.castSucc = x i := by
63   change (Fin.snoc x 0 : Stage (n+1)) i.castSucc = x i
64   simp
65 
66 @[simp] theorem insert_last (n : ℕ) (x : Stage n) :
67     insert n x (Fin.last (n+1)) = 0 := by
68   change (Fin.snoc x 0 : Stage (n+1)) (Fin.last (n+1)) = 0
69   simp
70 
71 theorem insert_opNorm (n : ℕ) : ‖insert n‖ ≤ 1 :=
72   ContinuousLinearMap.opNorm_le_bound _ zero_le_one
73     (fun x => by simpa only [insert, LinearMap.mkContinuous_apply, one_mul] using insertLinear_bound n x)
74 
75 theorem drop_insert (n : ℕ) : (drop n).comp (insert n) = ContinuousLinearMap.id ℝ (Stage n) := by
76   ext x i
77   simp
78 
79 /-- Both objects and bonding maps are genuinely level-dependent. -/
80 abbrev source : BanachTower ℝ where
81   Obj := Stage
82   down n := (1/2 : ℝ) • drop n
83   bound := 1/2
84   down_bound n := by
85     rw [norm_smul]
86     norm_num
87     nlinarith [drop_opNorm n]
88 
89 abbrev target : BanachTower ℝ where
90   Obj := Stage
91   down := drop
92   bound := 1
93   down_bound := drop_opNorm
94 
95 def targetSplitting : Splitting target where
96   up := insert
97   down_up := drop_insert
98   bound := 1
99   up_bound := insert_opNorm
100 
101 theorem propagation_gap :
102     (targetSplitting.bound : ℝ) * source.bound < 1 := by
103   norm_num [targetSplitting, source]
104 
105 theorem gain_eq_two : targetSplitting.gain source = 2 := by
106   norm_num [Splitting.gain, targetSplitting, source]
107 
108 def correction : Residuals source target →L[ℝ] Candidates source target :=
109   targetSplitting.correction source propagation_gap
110 
111 def exactRepair : Candidates source target →L[ℝ] Candidates source target :=
112   targetSplitting.repair source propagation_gap
113 
114 @[simp] theorem differential_correction (r : Residuals source target) :
115     differential source target (correction r) = r :=
116   targetSplitting.differential_correction source propagation_gap r
117 
118 theorem correction_bound (r : Residuals source target) : ‖correction r‖ ≤ 2 * ‖r‖ := by
119   simpa only [gain_eq_two, correction] using targetSplitting.correction_bound source propagation_gap r
120 
121 theorem exactRepair_exact (f : Candidates source target) : Exact source target (exactRepair f) :=
122   targetSplitting.repair_exact source propagation_gap f
123 
124 theorem exactRepair_error (f : Candidates source target) :
125     ‖f - exactRepair f‖ ≤ 2 * ‖differential source target f‖ := by
126   simpa only [gain_eq_two, exactRepair] using targetSplitting.repair_error source propagation_gap f
127 
128 @[simp] theorem exactRepair_seed (f : Candidates source target) : exactRepair f 0 = f 0 :=
129   targetSplitting.repair_preserves_zero source propagation_gap f
130 
131 /-- The correction never erases the newly added target row. -/
132 @[simp] theorem correction_last (r : Residuals source target) (n : ℕ) (x : Stage (n+1)) :
133     correction r (n+1) x (Fin.last (n+1)) = 0 := by
134   change insert n _ (Fin.last (n+1)) = 0
135   exact insert_last n _
136 
137 /-- Every newly exposed output row is preserved by the repair. -/
138 theorem exactRepair_last (f : Candidates source target) (n : ℕ) (x : Stage (n+1)) :
139     exactRepair f (n+1) x (Fin.last (n+1)) = f (n+1) x (Fin.last (n+1)) := by
140   change f (n+1) x (Fin.last (n+1)) -
141     correction (differential source target f) (n+1) x (Fin.last (n+1)) = _
142   rw [correction_last, sub_zero]
143 
144 /-- A non-exact input with nonzero protected seed and nonzero innovation at every stage. -/
145 def identityCandidate : Candidates source target :=
146   ⟨fun n => ContinuousLinearMap.id ℝ (Stage n), memℓp_infty ⟨1, by
147     rintro _ ⟨n, rfl⟩
148     exact ContinuousLinearMap.norm_id_le⟩⟩
149 
150 @[simp] theorem identityCandidate_apply (n : ℕ) (x : Stage n) : identityCandidate n x = x := rfl
151 
152 theorem identityCandidate_defect (n : ℕ) :
153     differential source target identityCandidate n = (1/2 : ℝ) • drop n := by
154   ext x i
155   change x i.castSucc - (1/2 : ℝ) * x i.castSucc = (1/2 : ℝ) * x i.castSucc
156   ring
157 
158 theorem identityCandidate_not_exact : ¬ Exact source target identityCandidate := by
159   intro he
160   have hz := (exact_iff_differential_zero source target identityCandidate).mp he
161   have h := congrArg (fun r : Residuals source target => r 0 (fun _ => 1) 0) hz
162   change (1 : ℝ) - (1/2 : ℝ) * 1 = 0 at h
163   norm_num at h
164 
165 theorem identityRepair_nonzero : exactRepair identityCandidate ≠ 0 := by
166   intro hz
167   have h := congrArg (fun f : Candidates source target => f 0 (fun _ => 1) 0) hz
168   rw [exactRepair_seed] at h
169   change (1 : ℝ) = 0 at h
170   norm_num at h
171 
172 /-- The first repair already changes inherited data while retaining new data. -/
173 theorem identityRepair_first_old (x : Stage 1) :
174     exactRepair identityCandidate 1 x 0 = (1/2 : ℝ) * x 0 := by
175   change x 0 - insert 0 ((differential source target identityCandidate 0 +
176     (0 : Stage 0 →L[ℝ] Stage 0).comp (source.down 0)) x) 0 = _
177   rw [identityCandidate_defect]
178   simp [insert, insertLinear, drop_apply, smul_eq_mul]
179   ring
180 
181 theorem identityRepair_first_new (x : Stage 1) : exactRepair identityCandidate 1 x 1 = x 1 :=
182   exactRepair_last identityCandidate 0 x
183 
184 /-- Exact compatibility transports every inherited row by the source contraction. -/
185 theorem exactRepair_old (f : Candidates source target) (n : ℕ)
186     (x : Stage (n+1)) (i : Fin (n+1)) :
187     exactRepair f (n+1) x i.castSucc = (1/2 : ℝ) * exactRepair f n (drop n x) i := by
188   have h := congrArg (fun T : Stage (n+1) →L[ℝ] Stage n => T x i)
189     (exactRepair_exact f n)
190   change exactRepair f (n+1) x i.castSucc = exactRepair f n ((1/2 : ℝ) • drop n x) i at h
191   rw [map_smul] at h
192   exact h
193 
194 /-- An all-level closed formula for the repair of the initially incompatible identities. -/
195 theorem identityRepair_formula (n : ℕ) : ∀ (x : Stage n) (i : Fin (n+1)),
196     exactRepair identityCandidate n x i = (1/2 : ℝ) ^ (n-i.val) * x i := by
197   induction n with
198   | zero =>
199     intro x i
200     simp only [Nat.zero_sub, pow_zero, one_mul]
201     rw [exactRepair_seed]
202     rfl
203   | succ n ih =>
204     intro x i
205     refine Fin.lastCases ?_ (fun j => ?_) i
206     · simp only [Fin.val_last, Nat.sub_self, pow_zero, one_mul]
207       exact exactRepair_last identityCandidate n x
208     · rw [exactRepair_old, ih]
209       have hn : n+1-j.val = (n-j.val)+1 := by omega
210       rw [Fin.val_castSucc, hn, pow_succ, drop_apply]
211       ring
212 
213 /-- Realization is a map of the actual inverse-limit point types. -/
214 def realizedIdentity : source.Point → target.Point :=
215   onLimit source target (exactRepair identityCandidate) (exactRepair_exact identityCandidate)
216 
217 @[simp] theorem realizedIdentity_coordinate (x : source.Point) (n : ℕ) (i : Fin (n+1)) :
218     (realizedIdentity x).val n i = (1/2 : ℝ) ^ (n-i.val) * x.val n i :=
219   identityRepair_formula n (x.val n) i
220 
221 end GrowingTower
222 end KomorebiSpace
223 end

Back to source controls