LinearDefects.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 
6 import Mathlib.Analysis.Normed.Ring.Basic
7 import Mathlib.Tactic.NoncommRing
8 
9 /-!
10 # Paper II: algebraic linear defects
11 
12 Author: Komorebi P.
13 
14 This module records the noncommutative telescoping identity for a one-step
15 intertwining defect.  The identity is valid in every ring and for every
16 natural power, including power zero.  It also gives the corresponding norm
17 estimate in a normed ring and proves the inverse-sandwich identity from
18 explicit left- and right-inverse equations.
19 -/
20 
21 set_option autoImplicit false
22 
23 namespace Komorebi.PaperII.LinearDefects
24 
25 open scoped BigOperators
26 
27 universe u
28 
29 /-! ## Power defects -/
30 
31 /-- The one-step defect of `C` with respect to the fine operator `Tf` and
32 the coarse operator `Tc`. -/
33 def defect {R : Type u} [Ring R] (C Tf Tc : R) : R :=
34   C * Tf - Tc * C
35 
36 /-- The power-defect telescoping identity, including the case `n = 0`.
37 
38 No factors are commuted: the coarse powers remain on the left of the defect
39 and the fine powers remain on its right.
40 -/
41 theorem power_defect_identity_all {R : Type u} [Ring R]
42     (C Tf Tc : R) (n : ℕ) :
43     C * Tf ^ n - Tc ^ n * C =
44       ∑ k ∈ Finset.range n,
45         Tc ^ (n - 1 - k) * defect C Tf Tc * Tf ^ k := by
46   induction n with
47   | zero => simp [defect]
48   | succ n ih =>
49       rw [Finset.sum_range_succ]
50       calc
51         C * Tf ^ (n + 1) - Tc ^ (n + 1) * C =
52             Tc * (C * Tf ^ n - Tc ^ n * C) + defect C Tf Tc * Tf ^ n := by
53               simp only [defect, pow_succ']
54               noncomm_ring
55         _ = Tc * (∑ k ∈ Finset.range n,
56               Tc ^ (n - 1 - k) * defect C Tf Tc * Tf ^ k) +
57               defect C Tf Tc * Tf ^ n := by rw [ih]
58         _ = (∑ k ∈ Finset.range n,
59               Tc ^ ((n + 1) - 1 - k) * defect C Tf Tc * Tf ^ k) +
60               Tc ^ ((n + 1) - 1 - n) * defect C Tf Tc * Tf ^ n := by
61               congr 1
62               · rw [Finset.mul_sum]
63                 apply Finset.sum_congr rfl
64                 intro k hk
65                 have hklt : k < n := Finset.mem_range.mp hk
66                 have hexponent : n - 1 - k + 1 = n - k := by omega
67                 calc
68                   Tc * (Tc ^ (n - 1 - k) * defect C Tf Tc * Tf ^ k) =
69                       (Tc * Tc ^ (n - 1 - k)) * defect C Tf Tc * Tf ^ k := by
70                         simp only [mul_assoc]
71                   _ = Tc ^ (n - 1 - k + 1) * defect C Tf Tc * Tf ^ k := by
72                         rw [← pow_succ']
73                   _ = Tc ^ (n - k) * defect C Tf Tc * Tf ^ k := by
74                         rw [hexponent]
75                   _ = Tc ^ ((n + 1) - 1 - k) * defect C Tf Tc * Tf ^ k := by
76                         have hsucc : (n + 1) - 1 - k = n - k := by omega
77                         rw [hsucc]
78               · simp
79 
80 /-- The positive-power form used in Paper II. -/
81 theorem power_defect_identity {R : Type u} [Ring R]
82     (C Tf Tc : R) (n : ℕ) (_hn : 0 < n) :
83     C * Tf ^ n - Tc ^ n * C =
84       ∑ k ∈ Finset.range n,
85         Tc ^ (n - 1 - k) * defect C Tf Tc * Tf ^ k :=
86   power_defect_identity_all C Tf Tc n
87 
88 /-- Submultiplicativity turns the exact telescoping formula into the usual
89 power-defect estimate with the norms of the actual powers.  This form needs
90 only a `NormedRing`; neither completeness nor normalization of `‖1‖` is
91 required. -/
92 theorem norm_power_defect_le_raw {R : Type u} [NormedRing R]
93     (C Tf Tc : R) (n : ℕ) :
94     ‖C * Tf ^ n - Tc ^ n * C‖ ≤
95       ∑ k ∈ Finset.range n,
96         ‖defect C Tf Tc‖ *
97           (‖Tc ^ (n - 1 - k)‖ * ‖Tf ^ k‖) := by
98   rw [power_defect_identity_all]
99   calc
100     ‖∑ k ∈ Finset.range n,
101         Tc ^ (n - 1 - k) * defect C Tf Tc * Tf ^ k‖ ≤
102         ∑ k ∈ Finset.range n,
103           ‖Tc ^ (n - 1 - k) * defect C Tf Tc * Tf ^ k‖ :=
104       norm_sum_le _ _
105     _ ≤ ∑ k ∈ Finset.range n,
106           ‖defect C Tf Tc‖ *
107             (‖Tc ^ (n - 1 - k)‖ * ‖Tf ^ k‖) := by
108       apply Finset.sum_le_sum
109       intro k _hk
110       calc
111         ‖Tc ^ (n - 1 - k) * defect C Tf Tc * Tf ^ k‖ ≤
112             ‖Tc ^ (n - 1 - k) * defect C Tf Tc‖ * ‖Tf ^ k‖ :=
113           norm_mul_le _ _
114         _ ≤ (‖Tc ^ (n - 1 - k)‖ * ‖defect C Tf Tc‖) * ‖Tf ^ k‖ :=
115           mul_le_mul_of_nonneg_right (norm_mul_le _ _) (norm_nonneg _)
116         _ = ‖defect C Tf Tc‖ *
117             (‖Tc ^ (n - 1 - k)‖ * ‖Tf ^ k‖) := by
118           ac_rfl
119 
120 /-- For a normalized norm, the raw estimate becomes the power bound displayed
121 in Paper II.  Completeness is not required. -/
122 theorem norm_power_defect_le {R : Type u} [NormedRing R] [NormOneClass R]
123     (C Tf Tc : R) (n : ℕ) :
124     ‖C * Tf ^ n - Tc ^ n * C‖ ≤
125       ‖defect C Tf Tc‖ *
126         ∑ k ∈ Finset.range n, ‖Tc‖ ^ (n - 1 - k) * ‖Tf‖ ^ k := by
127   rw [power_defect_identity_all]
128   calc
129     ‖∑ k ∈ Finset.range n,
130         Tc ^ (n - 1 - k) * defect C Tf Tc * Tf ^ k‖ ≤
131         ∑ k ∈ Finset.range n,
132           ‖Tc ^ (n - 1 - k) * defect C Tf Tc * Tf ^ k‖ :=
133       norm_sum_le _ _
134     _ ≤ ∑ k ∈ Finset.range n,
135           ‖defect C Tf Tc‖ *
136             (‖Tc‖ ^ (n - 1 - k) * ‖Tf‖ ^ k) := by
137       apply Finset.sum_le_sum
138       intro k _hk
139       calc
140         ‖Tc ^ (n - 1 - k) * defect C Tf Tc * Tf ^ k‖ ≤
141             ‖Tc ^ (n - 1 - k) * defect C Tf Tc‖ * ‖Tf ^ k‖ :=
142           norm_mul_le _ _
143         _ ≤ (‖Tc ^ (n - 1 - k)‖ * ‖defect C Tf Tc‖) * ‖Tf ^ k‖ :=
144           mul_le_mul_of_nonneg_right (norm_mul_le _ _) (norm_nonneg _)
145         _ ≤ (‖Tc‖ ^ (n - 1 - k) * ‖defect C Tf Tc‖) * ‖Tf ^ k‖ :=
146           mul_le_mul_of_nonneg_right
147             (mul_le_mul_of_nonneg_right (norm_pow_le _ _) (norm_nonneg _))
148             (norm_nonneg _)
149         _ ≤ (‖Tc‖ ^ (n - 1 - k) * ‖defect C Tf Tc‖) * ‖Tf‖ ^ k :=
150           mul_le_mul_of_nonneg_left (norm_pow_le _ _)
151             (mul_nonneg (pow_nonneg (norm_nonneg _) _) (norm_nonneg _))
152         _ = ‖defect C Tf Tc‖ *
153             (‖Tc‖ ^ (n - 1 - k) * ‖Tf‖ ^ k) := by
154           ac_rfl
155     _ = ‖defect C Tf Tc‖ *
156           ∑ k ∈ Finset.range n, ‖Tc‖ ^ (n - 1 - k) * ‖Tf‖ ^ k := by
157       rw [Finset.mul_sum]
158 
159 /-! ## Explicit inverse witnesses -/
160 
161 /-- `xinv` is an explicitly supplied two-sided inverse of `x`.
162 
163 Both equations are retained because the ambient ring need not be
164 commutative.
165 -/
166 structure TwoSidedInverse {R : Type u} [Mul R] [One R]
167     (x xinv : R) : Prop where
168   left_inv : xinv * x = 1
169   right_inv : x * xinv = 1
170 
171 /-- The inverse-sandwich identity for two independently supplied inverse
172 witnesses. -/
173 theorem inverse_sandwich_identity {R : Type u} [Ring R]
174     (A Ainv B Binv C : R)
175     (hA : TwoSidedInverse A Ainv)
176     (hB : TwoSidedInverse B Binv) :
177     C * Binv - Ainv * C =
178       Ainv * (A * C - C * B) * Binv := by
179   calc
180     C * Binv - Ainv * C =
181         (Ainv * A) * (C * Binv) - (Ainv * C) * (B * Binv) := by
182           rw [hA.left_inv, hB.right_inv]
183           simp
184     _ = Ainv * (A * C - C * B) * Binv := by
185       noncomm_ring
186 
187 /-- The resolvent-defect identity in a possibly noncommutative ring.
188 
189 The hypothesis `Commute z C` expresses exactly the centrality needed of the
190 scalar shift.  In a commutative ring it is automatic.
191 -/
192 theorem resolvent_defect_identity {R : Type u} [Ring R]
193     (z C Tf Tc Rf Rc : R)
194     (hf : TwoSidedInverse (z - Tf) Rf)
195     (hc : TwoSidedInverse (z - Tc) Rc)
196     (hzC : Commute z C) :
197     C * Rf - Rc * C = Rc * defect C Tf Tc * Rf := by
198   have hmiddle : (z - Tc) * C - C * (z - Tf) = defect C Tf Tc := by
199     simp only [defect, sub_mul, mul_sub]
200     rw [hzC.eq]
201     noncomm_ring
202   calc
203     C * Rf - Rc * C =
204         Rc * ((z - Tc) * C - C * (z - Tf)) * Rf :=
205       inverse_sandwich_identity (z - Tc) Rc (z - Tf) Rf C hc hf
206     _ = Rc * defect C Tf Tc * Rf := by rw [hmiddle]
207 
208 end Komorebi.PaperII.LinearDefects

Back to source controls