ReleaseDefectTower.lean

1 import KomorebiVerification.PaperII.TypedLinearDefects
2 import Mathlib.Algebra.BigOperators.Fin
3 import Mathlib.Data.Nat.Basic
4 
5 set_option autoImplicit false
6 namespace Komorebi.PaperII.ReleaseDefectTower
7 open scoped BigOperators
8 open TypedLinearDefects
9 universe u v
10 
11 section Algebraic
12 variable {R : Type u} [Semiring R]
13 variable {X : ℕ → Type v} [∀ n, AddCommGroup (X n)] [∀ n, Module R (X n)]
14 
15 /-- The actual ordered composite C_a C_(a+1) ... C_(b-1).
16 The dependent source and target retain every state space of the tower. -/
17 def segment (C : ∀ n, X (n + 1) →ₗ[R] X n) {a b : ℕ} (h : a ≤ b) :
18     X b →ₗ[R] X a :=
19   Nat.leRecOn (C := fun n => X n →ₗ[R] X a) h
20     (fun {n} f => f.comp (C n)) LinearMap.id
21 
22 @[simp] theorem segment_self (C : ∀ n, X (n + 1) →ₗ[R] X n) (a : ℕ) :
23     segment C (Nat.le_refl a) = LinearMap.id := by
24   exact Nat.leRecOn_self _
25 
26 theorem segment_succ (C : ∀ n, X (n + 1) →ₗ[R] X n)
27     {a b : ℕ} (h : a ≤ b) (hs : a ≤ b + 1) :
28     segment C hs = (segment C h).comp (C b) := by
29   exact Nat.leRecOn_succ h _
30 
31 /-- Each summand is the local defect transported by the actual preceding and
32 following comparison composites. -/
33 def localTerm (C : ∀ n, X (n + 1) →ₗ[R] X n)
34     (T : ∀ n, Module.End R (X n)) (L : ℕ) (k : Fin L) : X L →ₗ[R] X 0 :=
35   (segment C (Nat.zero_le k.val)).comp
36     ((defect (C k.val) (T (k.val + 1)) (T k.val)).comp
37       (segment C (Nat.succ_le_of_lt k.isLt)))
38 
39 /-- Arbitrary-length typed multilevel defect decomposition, including L=0. -/
40 theorem multilevel_defect (C : ∀ n, X (n + 1) →ₗ[R] X n)
41     (T : ∀ n, Module.End R (X n)) (L : ℕ) :
42     (segment C (Nat.zero_le L)).comp (T L) -
43         (T 0).comp (segment C (Nat.zero_le L)) =
44       ∑ k : Fin L, localTerm C T L k := by
45   induction L with
46   | zero => simp [localTerm]
47   | succ L ih =>
48       have hrec :
49           (segment C (Nat.zero_le (L + 1))).comp (T (L + 1)) -
50               (T 0).comp (segment C (Nat.zero_le (L + 1))) =
51             ((segment C (Nat.zero_le L)).comp (T L) -
52               (T 0).comp (segment C (Nat.zero_le L))).comp (C L) +
53               (segment C (Nat.zero_le L)).comp (defect (C L) (T (L + 1)) (T L)) := by
54         rw [segment_succ C (Nat.zero_le L)]
55         ext x
56         simp only [LinearMap.comp_apply, LinearMap.sub_apply,
57           LinearMap.add_apply, defect, map_sub]
58         abel
59       rw [hrec, ih, Fin.sum_univ_castSucc]
60       congr 1
61       · ext x
62         simp only [LinearMap.comp_apply, LinearMap.sum_apply]
63         apply Finset.sum_congr rfl
64         intro k hk
65         simp only [localTerm, Fin.val_castSucc]
66         rw [segment_succ C (Nat.succ_le_of_lt k.isLt)]
67         rfl
68       · simp [localTerm]
69 
70 /-- Zero local defects imply a zero total defect. -/
71 theorem multilevel_compatible (C : ∀ n, X (n + 1) →ₗ[R] X n)
72     (T : ∀ n, Module.End R (X n)) (L : ℕ)
73     (h : ∀ k : Fin L, defect (C k.val) (T (k.val + 1)) (T k.val) = 0) :
74     (segment C (Nat.zero_le L)).comp (T L) =
75       (T 0).comp (segment C (Nat.zero_le L)) := by
76   apply sub_eq_zero.mp
77   rw [multilevel_defect]
78   apply Finset.sum_eq_zero
79   intro k hk
80   simp [localTerm, h k]
81 /-- The polynomial consequence at arbitrary tower depth. -/
82 theorem multilevel_polynomial_compatible
83     {S : Type*} [CommSemiring S]
84     {Y : ℕ → Type*} [∀ n, AddCommGroup (Y n)] [∀ n, Module S (Y n)]
85     (C : ∀ n, Y (n + 1) →ₗ[S] Y n) (T : ∀ n, Module.End S (Y n))
86     (L : ℕ) (h : ∀ k : Fin L, defect (C k.val) (T (k.val + 1)) (T k.val) = 0)
87     (p : Polynomial S) :
88     (segment C (Nat.zero_le L)).comp (polynomialAction p (T L)) =
89       (polynomialAction p (T 0)).comp (segment C (Nat.zero_le L)) := by
90   apply polynomialAction_compatible_of_defect_eq_zero
91   exact sub_eq_zero.mpr (multilevel_compatible C T L h)
92 end Algebraic
93 
94 section Continuous
95 variable {𝕜 : Type u} [NontriviallyNormedField 𝕜]
96 variable {X : ℕ → Type v}
97 variable [∀ n, NormedAddCommGroup (X n)] [∀ n, NormedSpace 𝕜 (X n)]
98 
99 /-- The bounded actual segment composite in a typed tower. -/
100 def continuousSegment (C : ∀ n, X (n + 1) →L[𝕜] X n) {a b : ℕ} (h : a ≤ b) :
101     X b →L[𝕜] X a :=
102   Nat.leRecOn (C := fun n => X n →L[𝕜] X a) h
103     (fun {n} f => f.comp (C n)) (ContinuousLinearMap.id 𝕜 (X a))
104 
105 @[simp] theorem continuousSegment_self
106     (C : ∀ n, X (n + 1) →L[𝕜] X n) (a : ℕ) :
107     continuousSegment C (Nat.le_refl a) = ContinuousLinearMap.id 𝕜 (X a) := by
108   exact Nat.leRecOn_self _
109 
110 theorem continuousSegment_succ (C : ∀ n, X (n + 1) →L[𝕜] X n)
111     {a b : ℕ} (h : a ≤ b) (hs : a ≤ b + 1) :
112     continuousSegment C hs = (continuousSegment C h).comp (C b) := by
113   exact Nat.leRecOn_succ h _
114 
115 @[simp] theorem continuousSegment_toLinearMap
116     (C : ∀ n, X (n + 1) →L[𝕜] X n) {a b : ℕ} (h : a ≤ b) :
117     (continuousSegment C h).toLinearMap = segment (fun n => (C n).toLinearMap) h := by
118   induction b, h using Nat.le_induction with
119   | base => simp
120   | succ b hab ih =>
121       rw [continuousSegment_succ C hab, segment_succ _ hab]
122       simp only [ContinuousLinearMap.toLinearMap_comp, ih]
123 
124 /-- Normed local contribution with the same ordered factors as the manuscript. -/
125 def continuousLocalTerm (C : ∀ n, X (n + 1) →L[𝕜] X n)
126     (T : ∀ n, X n →L[𝕜] X n) (L : ℕ) (k : Fin L) : X L →L[𝕜] X 0 :=
127   (continuousSegment C (Nat.zero_le k.val)).comp
128     ((continuousDefect (C k.val) (T (k.val + 1)) (T k.val)).comp
129       (continuousSegment C (Nat.succ_le_of_lt k.isLt)))
130 
131 /-- Continuous-map version of the arbitrary-length typed telescope. -/
132 theorem continuous_multilevel_defect (C : ∀ n, X (n + 1) →L[𝕜] X n)
133     (T : ∀ n, X n →L[𝕜] X n) (L : ℕ) :
134     (continuousSegment C (Nat.zero_le L)).comp (T L) -
135         (T 0).comp (continuousSegment C (Nat.zero_le L)) =
136       ∑ k : Fin L, continuousLocalTerm C T L k := by
137   apply ContinuousLinearMap.coe_injective
138   simpa only [ContinuousLinearMap.toLinearMap_sub,
139     ContinuousLinearMap.toLinearMap_comp, ContinuousLinearMap.toLinearMap_sum,
140     continuousSegment_toLinearMap, continuousLocalTerm, localTerm,
141     continuousDefect_toLinearMap] using
142     (multilevel_defect (fun n => (C n).toLinearMap) (fun n => (T n).toLinearMap) L)
143 
144 /-- The multilevel norm estimate retains norms of the actual whole composites. -/
145 theorem continuous_norm_multilevel_defect_le
146     (C : ∀ n, X (n + 1) →L[𝕜] X n)
147     (T : ∀ n, X n →L[𝕜] X n) (L : ℕ) :
148     ‖(continuousSegment C (Nat.zero_le L)).comp (T L) -
149         (T 0).comp (continuousSegment C (Nat.zero_le L))‖ ≤
150       ∑ k : Fin L, ‖continuousSegment C (Nat.zero_le k.val)‖ *
151         ‖continuousDefect (C k.val) (T (k.val + 1)) (T k.val)‖ *
152         ‖continuousSegment C (Nat.succ_le_of_lt k.isLt)‖ := by
153   rw [continuous_multilevel_defect]
154   refine (norm_sum_le _ _).trans ?_
155   apply Finset.sum_le_sum
156   intro k hk
157   unfold continuousLocalTerm
158   calc
159     _ ≤ ‖continuousSegment C (Nat.zero_le k.val)‖ *
160         ‖(continuousDefect (C k.val) (T (k.val + 1)) (T k.val)).comp
161           (continuousSegment C (Nat.succ_le_of_lt k.isLt))‖ :=
162       ContinuousLinearMap.opNorm_comp_le _ _
163     _ ≤ ‖continuousSegment C (Nat.zero_le k.val)‖ *
164         (‖continuousDefect (C k.val) (T (k.val + 1)) (T k.val)‖ *
165           ‖continuousSegment C (Nat.succ_le_of_lt k.isLt)‖) :=
166       mul_le_mul_of_nonneg_left (ContinuousLinearMap.opNorm_comp_le _ _) (norm_nonneg _)
167     _ = _ := (mul_assoc _ _ _).symm
168 /-- Vanishing local continuous defects imply exact total compatibility. -/
169 theorem continuous_multilevel_compatible
170     (C : ∀ n, X (n + 1) →L[𝕜] X n) (T : ∀ n, X n →L[𝕜] X n)
171     (L : ℕ) (h : ∀ k : Fin L,
172       continuousDefect (C k.val) (T (k.val + 1)) (T k.val) = 0) :
173     (continuousSegment C (Nat.zero_le L)).comp (T L) =
174       (T 0).comp (continuousSegment C (Nat.zero_le L)) := by
175   apply sub_eq_zero.mp
176   rw [continuous_multilevel_defect]
177   apply Finset.sum_eq_zero
178   intro k hk
179   simp [continuousLocalTerm, h k]
180 
181 /-- Arbitrary-depth continuous polynomial compatibility. -/
182 theorem continuous_multilevel_polynomial_compatible
183     (C : ∀ n, X (n + 1) →L[𝕜] X n) (T : ∀ n, X n →L[𝕜] X n)
184     (L : ℕ) (h : ∀ k : Fin L,
185       continuousDefect (C k.val) (T (k.val + 1)) (T k.val) = 0)
186     (p : Polynomial 𝕜) :
187     (continuousSegment C (Nat.zero_le L)).comp (continuousPolynomialAction p (T L)) =
188       (continuousPolynomialAction p (T 0)).comp (continuousSegment C (Nat.zero_le L)) := by
189   apply continuousPolynomialAction_compatible_of_defect_eq_zero
190   exact sub_eq_zero.mpr (continuous_multilevel_compatible C T L h)
191 
192 /-- Arbitrary-depth resolvent compatibility with explicit one-sided witnesses. -/
193 theorem continuous_multilevel_resolvents_compatible
194     (C : ∀ n, X (n + 1) →L[𝕜] X n) (T : ∀ n, X n →L[𝕜] X n)
195     (L : ℕ) (h : ∀ k : Fin L,
196       continuousDefect (C k.val) (T (k.val + 1)) (T k.val) = 0)
197     (z : 𝕜) (Rf : X L →L[𝕜] X L) (Rc : X 0 →L[𝕜] X 0)
198     (hf : (continuousScalarShift z (T L)).comp Rf = 1)
199     (hc : Rc.comp (continuousScalarShift z (T 0)) = 1) :
200     (continuousSegment C (Nat.zero_le L)).comp Rf =
201       Rc.comp (continuousSegment C (Nat.zero_le L)) := by
202   apply continuous_resolvents_compatible_of_defect_eq_zero z _ (T L) Rf (T 0) Rc hf hc
203   exact sub_eq_zero.mpr (continuous_multilevel_compatible C T L h)
204 end Continuous
205 end Komorebi.PaperII.ReleaseDefectTower

Back to source controls