TypedLinearDefects.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 
6 import Mathlib.Algebra.BigOperators.Intervals
7 import Mathlib.Algebra.Module.Submodule.LinearMap
8 import Mathlib.Algebra.Polynomial.Eval.Defs
9 import Mathlib.Analysis.Normed.Operator.Basic
10 import Mathlib.Tactic.Abel
11 
12 /-!
13 # Paper II: typed linear defects
14 
15 Author: Komorebi P.
16 
17 The fine and coarse state spaces in this file are genuinely different
18 modules.  Thus the coarsening map cannot be silently treated as an
19 endomorphism.  We define its one-step intertwining defect, telescope that
20 defect through every natural power, and derive the scalar-shift resolvent
21 identity from explicit two-sided inverse witnesses.
22 -/
23 
24 set_option autoImplicit false
25 
26 namespace Komorebi.PaperII.TypedLinearDefects
27 
28 open scoped BigOperators
29 
30 universe u v w
31 
32 variable {R : Type u} [Semiring R]
33 variable {Xf : Type v} {Xc : Type w}
34 variable [AddCommGroup Xf] [AddCommGroup Xc]
35 variable [Module R Xf] [Module R Xc]
36 
37 /-! ## Typed power defects -/
38 
39 /-- The typed one-step defect `C ∘ Tf - Tc ∘ C`. -/
40 def defect (C : Xf →ₗ[R] Xc)
41     (Tf : Module.End R Xf) (Tc : Module.End R Xc) : Xf →ₗ[R] Xc :=
42   C.comp Tf - Tc.comp C
43 
44 /-- The typed power-defect identity for every natural `n`, including zero. -/
45 theorem power_defect_identity_all
46     (C : Xf →ₗ[R] Xc) (Tf : Module.End R Xf) (Tc : Module.End R Xc)
47     (n : ℕ) :
48     C.comp (Tf ^ n) - (Tc ^ n).comp C =
49       ∑ k ∈ Finset.range n,
50         (Tc ^ (n - 1 - k)).comp ((defect C Tf Tc).comp (Tf ^ k)) := by
51   induction n with
52   | zero => simp [defect, Module.End.one_eq_id]
53   | succ n ih =>
54       have hrecurrence :
55           C.comp (Tf ^ (n + 1)) - (Tc ^ (n + 1)).comp C =
56             Tc.comp (C.comp (Tf ^ n) - (Tc ^ n).comp C) +
57               (defect C Tf Tc).comp (Tf ^ n) := by
58         ext x
59         simp only [pow_succ', Module.End.mul_apply, LinearMap.sub_apply,
60           LinearMap.add_apply, LinearMap.comp_apply, defect, map_sub]
61         abel
62       rw [Finset.sum_range_succ]
63       calc
64         C.comp (Tf ^ (n + 1)) - (Tc ^ (n + 1)).comp C =
65             Tc.comp (C.comp (Tf ^ n) - (Tc ^ n).comp C) +
66               (defect C Tf Tc).comp (Tf ^ n) := hrecurrence
67         _ = Tc.comp (∑ k ∈ Finset.range n,
68               (Tc ^ (n - 1 - k)).comp
69                 ((defect C Tf Tc).comp (Tf ^ k))) +
70               (defect C Tf Tc).comp (Tf ^ n) := by rw [ih]
71         _ = (∑ k ∈ Finset.range n,
72               (Tc ^ ((n + 1) - 1 - k)).comp
73                 ((defect C Tf Tc).comp (Tf ^ k))) +
74               (Tc ^ ((n + 1) - 1 - n)).comp
75                 ((defect C Tf Tc).comp (Tf ^ n)) := by
76           congr 1
77           · ext x
78             simp only [LinearMap.comp_apply, LinearMap.sum_apply, map_sum]
79             apply Finset.sum_congr rfl
80             intro k hk
81             have hklt : k < n := Finset.mem_range.mp hk
82             have hexponent : n - 1 - k + 1 = n - k := by omega
83             have hsucc : (n + 1) - 1 - k = n - k := by omega
84             rw [hsucc, ← hexponent]
85             change (Tc * Tc ^ (n - 1 - k))
86                 ((defect C Tf Tc) ((Tf ^ k) x)) =
87               (Tc ^ (n - 1 - k + 1))
88                 ((defect C Tf Tc) ((Tf ^ k) x))
89             rw [← pow_succ']
90           · simp [Module.End.one_eq_id]
91 
92 /-- The positive-power specialization stated in Paper II. -/
93 theorem power_defect_identity
94     (C : Xf →ₗ[R] Xc) (Tf : Module.End R Xf) (Tc : Module.End R Xc)
95     (n : ℕ) (_hn : 0 < n) :
96     C.comp (Tf ^ n) - (Tc ^ n).comp C =
97       ∑ k ∈ Finset.range n,
98         (Tc ^ (n - 1 - k)).comp ((defect C Tf Tc).comp (Tf ^ k)) :=
99   power_defect_identity_all C Tf Tc n
100 
101 /-- A zero one-step defect gives exact compatibility with every power. -/
102 theorem powers_compatible_of_defect_eq_zero
103     (C : Xf →ₗ[R] Xc) (Tf : Module.End R Xf) (Tc : Module.End R Xc)
104     (hdefect : defect C Tf Tc = 0) (n : ℕ) :
105     C.comp (Tf ^ n) = (Tc ^ n).comp C := by
106   apply sub_eq_zero.mp
107   rw [power_defect_identity_all]
108   simp [hdefect]
109 
110 /-! ## Typed polynomial functional calculus -/
111 
112 /-- The finite polynomial functional calculus for a module endomorphism.
113 
114 This explicit coefficient sum works for a possibly noncommutative
115 endomorphism ring; its scalar coefficients act centrally because the base
116 ring is commutative.
117 -/
118 def polynomialAction
119     {S : Type*} [CommSemiring S]
120     {M : Type*} [AddCommMonoid M] [Module S M]
121     (p : Polynomial S) (T : Module.End S M) : Module.End S M :=
122   p.sum fun n a => a • T ^ n
123 
124 /-- Exact one-step intertwining implies compatibility with every polynomial
125 in the fine and coarse operators. -/
126 theorem polynomialAction_compatible_of_defect_eq_zero
127     {S : Type*} [CommSemiring S]
128     {Mf : Type v} {Mc : Type w}
129     [AddCommGroup Mf] [AddCommGroup Mc] [Module S Mf] [Module S Mc]
130     (C : Mf →ₗ[S] Mc) (Tf : Module.End S Mf) (Tc : Module.End S Mc)
131     (hdefect : defect C Tf Tc = 0) (p : Polynomial S) :
132     C.comp (polynomialAction p Tf) =
133       (polynomialAction p Tc).comp C := by
134   classical
135   ext x
136   simp only [polynomialAction, Polynomial.sum_def, LinearMap.comp_apply,
137     LinearMap.sum_apply, map_sum, LinearMap.smul_apply, map_smul]
138   apply Finset.sum_congr rfl
139   intro n hn
140   rw [show C ((Tf ^ n) x) = (Tc ^ n) (C x) by
141     exact LinearMap.congr_fun
142       (powers_compatible_of_defect_eq_zero C Tf Tc hdefect n) x]
143 
144 /-! ## Continuous linear maps and the operator-norm bound -/
145 
146 variable {𝕜 : Type u} [NontriviallyNormedField 𝕜]
147 variable {Ef : Type v} {Ec : Type w}
148 variable [NormedAddCommGroup Ef] [NormedAddCommGroup Ec]
149 variable [NormedSpace 𝕜 Ef] [NormedSpace 𝕜 Ec]
150 
151 /-- The genuinely typed continuous defect `C ∘ Tf - Tc ∘ C`. -/
152 def continuousDefect (C : Ef →L[𝕜] Ec)
153     (Tf : Ef →L[𝕜] Ef) (Tc : Ec →L[𝕜] Ec) : Ef →L[𝕜] Ec :=
154   C.comp Tf - Tc.comp C
155 
156 /-- Forgetting continuity sends the continuous defect to the algebraic typed
157 defect without changing the formula. -/
158 @[simp]
159 theorem continuousDefect_toLinearMap
160     (C : Ef →L[𝕜] Ec) (Tf : Ef →L[𝕜] Ef) (Tc : Ec →L[𝕜] Ec) :
161     (continuousDefect C Tf Tc : Ef →ₗ[𝕜] Ec) =
162       defect C.toLinearMap Tf.toLinearMap Tc.toLinearMap := by
163   rfl
164 
165 /-- The continuous-linear-map power-defect identity for every natural power.
166 
167 The proof is a faithful bridge to `power_defect_identity_all`; injectivity of
168 the forgetful map shows that no continuity information is lost.
169 -/
170 theorem continuous_power_defect_identity_all
171     (C : Ef →L[𝕜] Ec) (Tf : Ef →L[𝕜] Ef) (Tc : Ec →L[𝕜] Ec)
172     (n : ℕ) :
173     C.comp (Tf ^ n) - (Tc ^ n).comp C =
174       ∑ k ∈ Finset.range n,
175         (Tc ^ (n - 1 - k)).comp
176           ((continuousDefect C Tf Tc).comp (Tf ^ k)) := by
177   apply ContinuousLinearMap.coe_injective
178   simpa only [ContinuousLinearMap.toLinearMap_sub,
179     ContinuousLinearMap.toLinearMap_comp,
180     ContinuousLinearMap.toLinearMap_pow,
181     ContinuousLinearMap.toLinearMap_sum,
182     continuousDefect_toLinearMap] using
183     (power_defect_identity_all C.toLinearMap Tf.toLinearMap Tc.toLinearMap n)
184 
185 /-- The positive-power continuous specialization stated in the manuscript. -/
186 theorem continuous_power_defect_identity
187     (C : Ef →L[𝕜] Ec) (Tf : Ef →L[𝕜] Ef) (Tc : Ec →L[𝕜] Ec)
188     (n : ℕ) (_hn : 0 < n) :
189     C.comp (Tf ^ n) - (Tc ^ n).comp C =
190       ∑ k ∈ Finset.range n,
191         (Tc ^ (n - 1 - k)).comp
192           ((continuousDefect C Tf Tc).comp (Tf ^ k)) :=
193   continuous_power_defect_identity_all C Tf Tc n
194 
195 /-- Powers of a continuous endomorphism satisfy the usual operator-norm
196 bound, including exponent zero.  The zero case uses `‖id‖ ≤ 1`, so this
197 does not require the state space to be nontrivial. -/
198 theorem continuous_end_pow_norm_le
199     {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
200     (T : E →L[𝕜] E) (n : ℕ) :
201     ‖T ^ n‖ ≤ ‖T‖ ^ n := by
202   cases n with
203   | zero =>
204       simpa only [pow_zero, ContinuousLinearMap.one_def] using
205         (ContinuousLinearMap.norm_id_le (𝕜 := 𝕜) (E := E))
206   | succ n =>
207       exact norm_pow_le' T (Nat.succ_pos n)
208 
209 /-- The manuscript's typed operator-norm power-defect estimate. -/
210 theorem continuous_norm_power_defect_le
211     (C : Ef →L[𝕜] Ec) (Tf : Ef →L[𝕜] Ef) (Tc : Ec →L[𝕜] Ec)
212     (n : ℕ) :
213     ‖C.comp (Tf ^ n) - (Tc ^ n).comp C‖ ≤
214       ‖continuousDefect C Tf Tc‖ *
215         ∑ k ∈ Finset.range n, ‖Tc‖ ^ (n - 1 - k) * ‖Tf‖ ^ k := by
216   rw [continuous_power_defect_identity_all]
217   calc
218     ‖∑ k ∈ Finset.range n,
219         (Tc ^ (n - 1 - k)).comp
220           ((continuousDefect C Tf Tc).comp (Tf ^ k))‖ ≤
221         ∑ k ∈ Finset.range n,
222           ‖(Tc ^ (n - 1 - k)).comp
223             ((continuousDefect C Tf Tc).comp (Tf ^ k))‖ :=
224       norm_sum_le _ _
225     _ ≤ ∑ k ∈ Finset.range n,
226           ‖continuousDefect C Tf Tc‖ *
227             (‖Tc‖ ^ (n - 1 - k) * ‖Tf‖ ^ k) := by
228       apply Finset.sum_le_sum
229       intro k _hk
230       calc
231         ‖(Tc ^ (n - 1 - k)).comp
232             ((continuousDefect C Tf Tc).comp (Tf ^ k))‖ ≤
233             ‖Tc ^ (n - 1 - k)‖ *
234               ‖(continuousDefect C Tf Tc).comp (Tf ^ k)‖ :=
235           ContinuousLinearMap.opNorm_comp_le _ _
236         _ ≤ ‖Tc ^ (n - 1 - k)‖ *
237               (‖continuousDefect C Tf Tc‖ * ‖Tf ^ k‖) :=
238           mul_le_mul_of_nonneg_left
239             (ContinuousLinearMap.opNorm_comp_le _ _) (norm_nonneg _)
240         _ ≤ ‖Tc‖ ^ (n - 1 - k) *
241               (‖continuousDefect C Tf Tc‖ * ‖Tf ^ k‖) :=
242           mul_le_mul_of_nonneg_right
243             (continuous_end_pow_norm_le Tc (n - 1 - k))
244             (mul_nonneg (norm_nonneg _) (norm_nonneg _))
245         _ ≤ ‖Tc‖ ^ (n - 1 - k) *
246               (‖continuousDefect C Tf Tc‖ * ‖Tf‖ ^ k) :=
247           mul_le_mul_of_nonneg_left
248             (mul_le_mul_of_nonneg_left
249               (continuous_end_pow_norm_le Tf k) (norm_nonneg _))
250             (pow_nonneg (norm_nonneg _) _)
251         _ = ‖continuousDefect C Tf Tc‖ *
252               (‖Tc‖ ^ (n - 1 - k) * ‖Tf‖ ^ k) := by
253           ac_rfl
254     _ = ‖continuousDefect C Tf Tc‖ *
255           ∑ k ∈ Finset.range n, ‖Tc‖ ^ (n - 1 - k) * ‖Tf‖ ^ k := by
256       rw [Finset.mul_sum]
257 
258 /-- If both dynamics have operator norm at most `ρ`, the `n`th typed defect
259 is bounded by the familiar linear-loss majorant
260 `n * ρ^(n-1) * ‖continuousDefect C Tf Tc‖`.
261 
262 The statement includes `n = 0`, where both sides vanish.
263 -/
264 theorem continuous_norm_power_defect_le_geometric_majorant
265     (C : Ef →L[𝕜] Ec) (Tf : Ef →L[𝕜] Ef) (Tc : Ec →L[𝕜] Ec)
266     (ρ : ℝ) (hTf : ‖Tf‖ ≤ ρ) (hTc : ‖Tc‖ ≤ ρ) (n : ℕ) :
267     ‖C.comp (Tf ^ n) - (Tc ^ n).comp C‖ ≤
268       (n : ℝ) * ρ ^ (n - 1) * ‖continuousDefect C Tf Tc‖ := by
269   cases n with
270   | zero => simp [ContinuousLinearMap.one_def]
271   | succ n =>
272       have hρ : 0 ≤ ρ := (norm_nonneg Tf).trans hTf
273       calc
274         ‖C.comp (Tf ^ (n + 1)) - (Tc ^ (n + 1)).comp C‖ ≤
275             ‖continuousDefect C Tf Tc‖ *
276               ∑ k ∈ Finset.range (n + 1),
277                 ‖Tc‖ ^ (n + 1 - 1 - k) * ‖Tf‖ ^ k :=
278           continuous_norm_power_defect_le C Tf Tc (n + 1)
279         _ ≤ ‖continuousDefect C Tf Tc‖ *
280               ∑ _k ∈ Finset.range (n + 1), ρ ^ n := by
281           apply mul_le_mul_of_nonneg_left _ (norm_nonneg _)
282           apply Finset.sum_le_sum
283           intro k hk
284           have hklt : k < n + 1 := Finset.mem_range.mp hk
285           calc
286             ‖Tc‖ ^ (n + 1 - 1 - k) * ‖Tf‖ ^ k ≤
287                 ρ ^ (n + 1 - 1 - k) * ρ ^ k := by
288               exact mul_le_mul
289                 (pow_le_pow_left₀ (norm_nonneg Tc) hTc _)
290                 (pow_le_pow_left₀ (norm_nonneg Tf) hTf _)
291                 (pow_nonneg (norm_nonneg Tf) _) (pow_nonneg hρ _)
292             _ = ρ ^ n := by
293               rw [← pow_add]
294               congr 1
295               omega
296         _ = (n + 1 : ℕ) * ρ ^ n * ‖continuousDefect C Tf Tc‖ := by
297           simp only [Finset.sum_const, Finset.card_range, nsmul_eq_mul]
298           push_cast
299           ring
300         _ = ((n + 1 : ℕ) : ℝ) * ρ ^ ((n + 1 : ℕ) - 1) *
301               ‖continuousDefect C Tf Tc‖ := by simp
302 
303 /-- A continuous zero defect gives exact compatibility with every power. -/
304 theorem continuous_powers_compatible_of_defect_eq_zero
305     (C : Ef →L[𝕜] Ec) (Tf : Ef →L[𝕜] Ef) (Tc : Ec →L[𝕜] Ec)
306     (hdefect : continuousDefect C Tf Tc = 0) (n : ℕ) :
307     C.comp (Tf ^ n) = (Tc ^ n).comp C := by
308   apply sub_eq_zero.mp
309   rw [continuous_power_defect_identity_all]
310   simp [hdefect]
311 
312 /-- The finite polynomial functional calculus for a continuous
313 endomorphism. -/
314 def continuousPolynomialAction
315     {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
316     (p : Polynomial 𝕜) (T : E →L[𝕜] E) : E →L[𝕜] E :=
317   p.sum fun n a => a • T ^ n
318 
319 /-- Vanishing continuous defect makes the coarsening map intertwine the
320 polynomial functional calculi of the fine and coarse dynamics. -/
321 theorem continuousPolynomialAction_compatible_of_defect_eq_zero
322     (C : Ef →L[𝕜] Ec) (Tf : Ef →L[𝕜] Ef) (Tc : Ec →L[𝕜] Ec)
323     (hdefect : continuousDefect C Tf Tc = 0) (p : Polynomial 𝕜) :
324     C.comp (continuousPolynomialAction p Tf) =
325       (continuousPolynomialAction p Tc).comp C := by
326   classical
327   ext x
328   simp only [continuousPolynomialAction, Polynomial.sum_def,
329     ContinuousLinearMap.comp_apply, sum_apply, map_sum, smul_apply, map_smul]
330   apply Finset.sum_congr rfl
331   intro n hn
332   rw [show C ((Tf ^ n) x) = (Tc ^ n) (C x) by
333     have h := continuous_powers_compatible_of_defect_eq_zero
334       C Tf Tc hdefect n
335     exact congrArg (fun F : Ef →L[𝕜] Ec => F x) h]
336 
337 /-! ## Typed inverse sandwiches and resolvents -/
338 
339 /-- An explicitly supplied two-sided inverse of a module endomorphism. -/
340 structure TwoSidedInverse {M : Type*} [AddCommGroup M] [Module R M]
341     (A Ainv : Module.End R M) : Prop where
342   left_inv : Ainv.comp A = LinearMap.id
343   right_inv : A.comp Ainv = LinearMap.id
344 
345 /-- The inverse-sandwich identity with different fine and coarse modules. -/
346 theorem inverse_sandwich_identity
347     (A Ainv : Module.End R Xc) (B Binv : Module.End R Xf)
348     (C : Xf →ₗ[R] Xc)
349     (hA : TwoSidedInverse A Ainv)
350     (hB : TwoSidedInverse B Binv) :
351     C.comp Binv - Ainv.comp C =
352       (Ainv.comp (A.comp C - C.comp B)).comp Binv := by
353   calc
354     C.comp Binv - Ainv.comp C =
355         (Ainv.comp A).comp (C.comp Binv) -
356           (Ainv.comp C).comp (B.comp Binv) := by
357       rw [hA.left_inv, hB.right_inv]
358       simp
359     _ = (Ainv.comp (A.comp C - C.comp B)).comp Binv := by
360       ext x
361       simp only [LinearMap.sub_apply, LinearMap.comp_apply, map_sub]
362 
363 /-- The endomorphism `z · id - T`. -/
364 def scalarShift {S : Type*} [CommSemiring S]
365     {M : Type*} [AddCommGroup M] [Module S M]
366     (z : S) (T : Module.End S M) : Module.End S M :=
367   z • (1 : Module.End S M) - T
368 
369 /-- The difference of the two typed scalar-shift composites is precisely the
370 one-step defect. -/
371 theorem scalarShift_comp_sub_comp_scalarShift
372     {S : Type*} [CommSemiring S]
373     {Mf : Type v} {Mc : Type w}
374     [AddCommGroup Mf] [AddCommGroup Mc] [Module S Mf] [Module S Mc]
375     (z : S) (C : Mf →ₗ[S] Mc)
376     (Tf : Module.End S Mf) (Tc : Module.End S Mc) :
377     (scalarShift z Tc).comp C - C.comp (scalarShift z Tf) =
378       defect C Tf Tc := by
379   ext x
380   simp only [scalarShift, defect, LinearMap.sub_apply, LinearMap.comp_apply,
381     LinearMap.smul_apply, Module.End.one_apply, map_sub, map_smul]
382   abel
383 
384 /-- The typed scalar-shift resolvent identity.
385 
386 `Rf` and `Rc` are concrete inverse candidates, and the two hypotheses expose
387 both inverse equations rather than relying on a partial inverse operation.
388 -/
389 theorem scalarShift_resolvent_identity
390     {S : Type*} [CommSemiring S]
391     {Mf : Type v} {Mc : Type w}
392     [AddCommGroup Mf] [AddCommGroup Mc] [Module S Mf] [Module S Mc]
393     (z : S) (C : Mf →ₗ[S] Mc)
394     (Tf Rf : Module.End S Mf) (Tc Rc : Module.End S Mc)
395     (hf : TwoSidedInverse (scalarShift z Tf) Rf)
396     (hc : TwoSidedInverse (scalarShift z Tc) Rc) :
397     C.comp Rf - Rc.comp C =
398       (Rc.comp (defect C Tf Tc)).comp Rf := by
399   calc
400     C.comp Rf - Rc.comp C =
401         (Rc.comp
402           ((scalarShift z Tc).comp C - C.comp (scalarShift z Tf))).comp Rf :=
403       inverse_sandwich_identity
404         (scalarShift z Tc) Rc (scalarShift z Tf) Rf C hc hf
405     _ = (Rc.comp (defect C Tf Tc)).comp Rf := by
406       rw [scalarShift_comp_sub_comp_scalarShift]
407 
408 /-- With zero defect, the explicitly witnessed fine and coarse resolvents
409 intertwine exactly. -/
410 theorem resolvents_compatible_of_defect_eq_zero
411     {S : Type*} [CommSemiring S]
412     {Mf : Type v} {Mc : Type w}
413     [AddCommGroup Mf] [AddCommGroup Mc] [Module S Mf] [Module S Mc]
414     (z : S) (C : Mf →ₗ[S] Mc)
415     (Tf Rf : Module.End S Mf) (Tc Rc : Module.End S Mc)
416     (hf : TwoSidedInverse (scalarShift z Tf) Rf)
417     (hc : TwoSidedInverse (scalarShift z Tc) Rc)
418     (hdefect : defect C Tf Tc = 0) :
419     C.comp Rf = Rc.comp C := by
420   apply sub_eq_zero.mp
421   rw [scalarShift_resolvent_identity z C Tf Rf Tc Rc hf hc, hdefect]
422   simp
423 
424 /-! ## Continuous typed resolvents and their norm estimate -/
425 
426 /-- The continuous endomorphism `z · id - T`. -/
427 def continuousScalarShift
428     (z : 𝕜) {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
429     (T : E →L[𝕜] E) : E →L[𝕜] E :=
430   z • (1 : E →L[𝕜] E) - T
431 
432 /-- The continuous scalar-shift commutator is the one-step defect. -/
433 theorem continuousScalarShift_comp_sub_comp_continuousScalarShift
434     (z : 𝕜) (C : Ef →L[𝕜] Ec)
435     (Tf : Ef →L[𝕜] Ef) (Tc : Ec →L[𝕜] Ec) :
436     (continuousScalarShift z Tc).comp C -
437         C.comp (continuousScalarShift z Tf) =
438       continuousDefect C Tf Tc := by
439   ext x
440   simp only [continuousScalarShift, continuousDefect,
441     sub_apply, ContinuousLinearMap.comp_apply, smul_apply, one_apply_eq_self,
442     map_sub, map_smul]
443   abel
444 
445 /-- The continuous inverse sandwich needs only the two one-sided inverse
446 equations that actually occur in the calculation: a left inverse for `A`
447 and a right inverse for `B`. -/
448 theorem continuous_inverse_sandwich_identity
449     (A Ainv : Ec →L[𝕜] Ec) (B Binv : Ef →L[𝕜] Ef)
450     (C : Ef →L[𝕜] Ec)
451     (hA : Ainv.comp A = 1) (hB : B.comp Binv = 1) :
452     C.comp Binv - Ainv.comp C =
453       (Ainv.comp (A.comp C - C.comp B)).comp Binv := by
454   calc
455     C.comp Binv - Ainv.comp C =
456         (Ainv.comp A).comp (C.comp Binv) -
457           (Ainv.comp C).comp (B.comp Binv) := by
458       ext x
459       simp only [sub_apply, ContinuousLinearMap.comp_apply]
460       have hAx : Ainv (A (C (Binv x))) = C (Binv x) := by
461         have h := congrArg (fun F : Ec →L[𝕜] Ec => F (C (Binv x))) hA
462         simpa only [ContinuousLinearMap.comp_apply,
463           one_apply_eq_self] using h
464       have hBx : B (Binv x) = x := by
465         have h := congrArg (fun F : Ef →L[𝕜] Ef => F x) hB
466         simpa only [ContinuousLinearMap.comp_apply,
467           one_apply_eq_self] using h
468       rw [hAx, hBx]
469     _ = (Ainv.comp (A.comp C - C.comp B)).comp Binv := by
470       ext x
471       simp only [sub_apply, ContinuousLinearMap.comp_apply, map_sub]
472 
473 /-- The continuous typed resolvent identity from explicit one-sided inverse
474 witnesses.  No global inverse operation or spectral hypothesis is hidden in
475 the statement. -/
476 theorem continuous_scalarShift_resolvent_identity
477     (z : 𝕜) (C : Ef →L[𝕜] Ec)
478     (Tf Rf : Ef →L[𝕜] Ef) (Tc Rc : Ec →L[𝕜] Ec)
479     (hf : (continuousScalarShift z Tf).comp Rf = 1)
480     (hc : Rc.comp (continuousScalarShift z Tc) = 1) :
481     C.comp Rf - Rc.comp C =
482       (Rc.comp (continuousDefect C Tf Tc)).comp Rf := by
483   calc
484     C.comp Rf - Rc.comp C =
485         (Rc.comp
486           ((continuousScalarShift z Tc).comp C -
487             C.comp (continuousScalarShift z Tf))).comp Rf :=
488       continuous_inverse_sandwich_identity
489         (continuousScalarShift z Tc) Rc
490         (continuousScalarShift z Tf) Rf C hc hf
491     _ = (Rc.comp (continuousDefect C Tf Tc)).comp Rf := by
492       rw [continuousScalarShift_comp_sub_comp_continuousScalarShift]
493 
494 /-- The analytic resolvent-defect estimate
495 `‖C Rf - Rc C‖ ≤ ‖Rc‖ ‖Δ‖ ‖Rf‖`. -/
496 theorem continuous_norm_resolvent_defect_le
497     (z : 𝕜) (C : Ef →L[𝕜] Ec)
498     (Tf Rf : Ef →L[𝕜] Ef) (Tc Rc : Ec →L[𝕜] Ec)
499     (hf : (continuousScalarShift z Tf).comp Rf = 1)
500     (hc : Rc.comp (continuousScalarShift z Tc) = 1) :
501     ‖C.comp Rf - Rc.comp C‖ ≤
502       ‖Rc‖ * ‖continuousDefect C Tf Tc‖ * ‖Rf‖ := by
503   rw [continuous_scalarShift_resolvent_identity z C Tf Rf Tc Rc hf hc]
504   calc
505     ‖(Rc.comp (continuousDefect C Tf Tc)).comp Rf‖ ≤
506         ‖Rc.comp (continuousDefect C Tf Tc)‖ * ‖Rf‖ :=
507       ContinuousLinearMap.opNorm_comp_le _ _
508     _ ≤ (‖Rc‖ * ‖continuousDefect C Tf Tc‖) * ‖Rf‖ :=
509       mul_le_mul_of_nonneg_right
510         (ContinuousLinearMap.opNorm_comp_le _ _) (norm_nonneg _)
511 
512 /-- With zero continuous defect, the explicit fine and coarse resolvents
513 intertwine exactly. -/
514 theorem continuous_resolvents_compatible_of_defect_eq_zero
515     (z : 𝕜) (C : Ef →L[𝕜] Ec)
516     (Tf Rf : Ef →L[𝕜] Ef) (Tc Rc : Ec →L[𝕜] Ec)
517     (hf : (continuousScalarShift z Tf).comp Rf = 1)
518     (hc : Rc.comp (continuousScalarShift z Tc) = 1)
519     (hdefect : continuousDefect C Tf Tc = 0) :
520     C.comp Rf = Rc.comp C := by
521   apply sub_eq_zero.mp
522   rw [continuous_scalarShift_resolvent_identity z C Tf Rf Tc Rc hf hc,
523     hdefect]
524   simp
525 
526 end Komorebi.PaperII.TypedLinearDefects

Back to source controls