05_defects.tex

Paper II: Refinement Towers, Weighted Transfer, and Integral Separation of Operator Packets

05_defects.tex

9 indexed statements in this file

These links follow the claim index. They do not extend the recorded proof or Lean coverage.

Download original file

This is the original TeX manuscript source. Use the paper’s PDF for typeset equations.

Read the typeset paper

Read this chapter with formatted equations

Skip source text

1 \section{Linear refinement defects}\label{sec:defects}
2 
3 Exact coordinate refinement describes two representations of the same object. In an application, the coarse operator may instead be chosen to model coarse dynamics. An intertwining defect measures the mismatch between applying the operator before or after passing to coarse coordinates.
4 
5 Let $X_f$ and $X_c$ be vector spaces or Banach spaces over a common field, and let
6 \[
7 C:X_f\longrightarrow X_c
8 \]
9 be a linear map,
10 and let
11 \[
12 T_f\in\End(X_f),
13 \qquad
14 T_c\in\End(X_c).
15 \]
16 Define
17 \[
18 \Delta=CT_f-T_cC.
19 \]
20 
21 \begin{keyidea}
22 There are two routes from a fine state to a coarse result. One applies the fine operator and then maps the result to the coarse space. The other maps the state first and then applies the coarse operator. The defect is the difference between these routes. Its vanishing says that the chosen operators are compatible with the comparison map. The norm estimates below combine the size of this defect with the norms of the surrounding operators.
23 \end{keyidea}
24 
Statement: Power defect identity · Go to proof · Read statement and proof side by side25 \begin{theorem}[Power defect identity]\label{thm:power_defect}\label{thm:power-defect}
26 For every integer $n\geq1$,
27 \[
28 CT_f^n-T_c^nC
29 =
30 \sum_{k=0}^{n-1}T_c^{n-1-k}\Delta T_f^k.
31 \]
32 \end{theorem}
33 
Proof block: Power defect identity · Go to statement · Read statement and proof side by side34 \begin{proof}
35 The statement is clear for $n=1$.  For the induction step, write
36 \[
37 CT_f^{n+1}-T_c^{n+1}C
38 =
39 (CT_f^n-T_c^nC)T_f+T_c^n(CT_f-T_cC)
40 \]
41 and apply the induction hypothesis.
42 \end{proof}
43 
Statement: Power norm bound · Go to proof · Read statement and proof side by side44 \begin{corollary}[Power norm bound]\label{cor:power_norm}
45 For bounded operators between Banach spaces,
46 \[
47 \|CT_f^n-T_c^nC\|
48 \leq
49 \|\Delta\|
50 \sum_{k=0}^{n-1}
51 \|T_c\|^{n-1-k}\|T_f\|^k.
52 \]
53 \end{corollary}
54 
Proof block: Power norm bound · Go to statement · Read statement and proof side by side55 \begin{proof}
56 Apply the triangle inequality and submultiplicativity to \cref{thm:power_defect}.
57 \end{proof}
58 
59 \Needspace{4\baselineskip}
Statement: Norm bound60 \begin{corollary}[Norm bound]\label{cor:defect-norm}
61 For a submultiplicative operator norm,
62 \[
63 \|CT_f^n-T_c^nC\|
64 \le
65 \|\Delta\|
66 \sum_{k=0}^{n-1}
67 \|T_c\|^{n-1-k}\|T_f\|^k.
68 \]
69 If $\|T_f\|,\|T_c\|\le\rho$, then
70 \[
71 \boxed{
72 \|CT_f^n-T_c^nC\|
73 \le n\rho^{n-1}\|\Delta\|.
74 }
75 \]
76 \end{corollary}
77 
Statement: Polynomial defect · Go to proof · Read statement and proof side by side78 \begin{corollary}[Polynomial defect]\label{cor:polynomial_defect}
79 For
80 \[
81 p(z)=\sum_{n=0}^Na_nz^n,
82 \]
83 we have
84 \[
85 Cp(T_f)-p(T_c)C
86 =
87 \sum_{n=1}^Na_n
88 \sum_{k=0}^{n-1}T_c^{n-1-k}\Delta T_f^k.
89 \]
90 \end{corollary}
91 
Proof block: Polynomial defect · Go to statement · Read statement and proof side by side92 \begin{proof}
93 The constant terms cancel because $CI=IC$.  Apply \cref{thm:power_defect} to every positive power and sum.
94 \end{proof}
95 
Statement: Resolvent defect identity · Go to proof · Read statement and proof side by side96 \begin{theorem}[Resolvent defect identity]\label{thm:resolvent_defect}\label{thm:resolvent-defect}
97 If $z-T_f$ and $z-T_c$ are invertible, then
98 \[
99 C(z-T_f)^{-1}-(z-T_c)^{-1}C
100 =
101 (z-T_c)^{-1}\Delta(z-T_f)^{-1}.
102 \]
103 \end{theorem}
104 
Proof block: Resolvent defect identity · Go to statement · Read statement and proof side by side105 \begin{proof}
106 Multiply the claimed identity on the left by $z-T_c$ and on the right by $z-T_f$.  The left side becomes
107 \[
108 (z-T_c)C-C(z-T_f)
109 =
110 CT_f-T_cC
111 =
112 \Delta.
113 \]
114 Multiplying back by the two resolvents proves the formula.
115 \end{proof}
116 
117 \subsection{Inverse witnesses from one side and norm control}
118 For continuous linear maps, the same identity gives the certified norm bound
119 \[
120 \boxed{
121 \|C R_f-R_c C\|
122 \le \|R_c\|\,\|\Delta\|\,\|R_f\|,
123 }
124 \]
125 from a left inverse witness for the coarse scalar shift and a right inverse
126 witness for the fine scalar shift. These witnesses suffice for the displayed
127 identity. On their own, they need not define inverses on both sides and hence
128 need not define resolvents. If $\Delta=0$, Lean also proves, for every finite
129 polynomial $p$, the exact compatibility
130 \[
131 \boxed{C\,p(T_f)=p(T_c)\,C,}
132 \]
133 in both the algebraic setting and the setting of continuous linear maps. Thus
134 all powers and polynomial actions intertwine with coarse reconstruction. The
135 stated inverse witnesses also intertwine. In particular, genuine resolvents
136 do so when the scalar shifts are invertible. This is the linear prototype
137 of the more general theory of refinement defects reserved for Paper III.
138 
139 \begin{figure}[htbp]
140 \centering
141 \includegraphics[width=0.96\textwidth]{09_refinement_defect_bound.pdf}
142 \caption{A controlled defect for one step and its telescoping norm bound under repeated operator application.}
143 \label{fig:defect-bound}
144 \end{figure}
145 
146 
147 \subsection{Analytic functional calculus}
Statement: Holomorphic functional calculus defect · Go to proof · Read statement and proof side by side148 \begin{theorem}[Holomorphic functional calculus defect]\label{thm:holomorphic_defect}
149 Let $X_f$ and $X_c$ be complex Banach spaces, and let $C:X_f\to X_c$, $T_f$, and $T_c$ be bounded complex-linear maps.  Let $h$ be holomorphic on an open set $U$ containing both spectra.  Let $\Gamma$ be an admissible finite rectifiable Cauchy cycle in $U$ and in both resolvent sets, with winding number one on the union of the spectra and zero outside $U$.  The length of a cycle counts multiplicities.  Then
150 \[
151 Ch(T_f)-h(T_c)C
152 =
153 \frac{1}{2\pi i}
154 \int_\Gamma
155 h(z)(z-T_c)^{-1}\Delta(z-T_f)^{-1}\,dz.
156 \]
157 Consequently,
158 \begin{align*}
159 \|Ch(T_f)-h(T_c)C\|
160 &\leq
161 \frac{\operatorname{length}(\Gamma)}{2\pi}
162 \sup_{z\in\Gamma}|h(z)|\,\|\Delta\|\\
163 &\quad\times
164 \sup_{z\in\Gamma}\|(z-T_c)^{-1}\|
165 \sup_{z\in\Gamma}\|(z-T_f)^{-1}\|.
166 \end{align*}
167 \end{theorem}
168 
Proof block: Holomorphic functional calculus defect · Go to statement · Read statement and proof side by side169 \begin{proof}
170 The assertion is immediate if either space is zero. Otherwise, use the rectifiable-cycle form of the holomorphic functional calculus in \cite[Chapter~VII, \S4, Theorem~4.1, formula~(4.5), and Proposition~4.6]{Conway1990}. For each operator $T$, compare $\Gamma$ with a positive simple system around its spectrum. Their difference has zero winding outside $U\setminus\sigma(T)$, so Theorem~4.1 applied to the resolvent-valued integrand identifies the two integrals. Consequently,
171 \[
172 h(T)
173 =
174 \frac{1}{2\pi i}
175 \int_\Gamma h(z)(z-T)^{-1}\,dz.
176 \]
177 Subtract the two formulas after composing with $C$, then use \cref{thm:resolvent_defect} inside the integral.  The norm estimate follows from the standard contour bound.
178 \end{proof}
179 
Statement: Exponential defect identity · Go to proof · Read statement and proof side by side180 \begin{theorem}[Exponential defect identity]\label{thm:exponential_defect}
181 Let $C:X_f\to X_c$, $T_f$, and $T_c$ be bounded linear maps between Banach spaces over a common field.  For real $t$, use real or complex spaces. For complex $t$, use complex spaces and complex-linear maps.  Then
182 \[
183 Ce^{tT_f}-e^{tT_c}C
184 =
185 \int_0^t e^{(t-s)T_c}\Delta e^{sT_f}\,ds,
186 \]
187 where the integral is taken along the straight segment from $0$ to $t$ when $t$ is complex.  For real $t\geq0$,
188 \[
189 \|Ce^{tT_f}-e^{tT_c}C\|
190 \leq
191 \|\Delta\|
192 \int_0^t
193 \|e^{(t-s)T_c}\|
194 \|e^{sT_f}\|\,ds.
195 \]
196 \end{theorem}
197 
Proof block: Exponential defect identity · Go to statement · Read statement and proof side by side198 \begin{proof}
199 For real $t$, differentiate
200 \[
201 F(s)=e^{(t-s)T_c}Ce^{sT_f}.
202 \]
203 We obtain
204 \[
205 F'(s)=e^{(t-s)T_c}\Delta e^{sT_f}.
206 \]
207 Integration from $0$ to $t$ gives the identity.  The complex statement follows by the same calculation along the straight segment.  The norm bound follows from the integral formula.
208 \end{proof}
209 
210 \subsection{Several refinement levels}
211 
212 Let
213 \[
214 C_\ell:X_{\ell+1}\longrightarrow X_\ell
215 \]
216 be linear maps for $0\leq\ell<L$, and let $T_\ell\in\End(X_\ell)$.  Put
217 \[
218 \Delta_\ell=C_\ell T_{\ell+1}-T_\ell C_\ell.
219 \]
220 For $a<b$, write
221 \[
222 C_{a,b}=C_aC_{a+1}\cdots C_{b-1},
223 \]
224 with $C_{a,a}=I$.
225 
Statement: Multilevel defect decomposition · Go to proof · Read statement and proof side by side226 \begin{theorem}[Multilevel defect decomposition]\label{thm:multilevel_defect}
227 The total defect from level $L$ to level zero is
228 \[
229 C_{0,L}T_L-T_0C_{0,L}
230 =
231 \sum_{\ell=0}^{L-1}
232 C_{0,\ell}\Delta_\ell C_{\ell+1,L}.
233 \]
234 For bounded maps,
235 \[
236 \|C_{0,L}T_L-T_0C_{0,L}\|
237 \leq
238 \sum_{\ell=0}^{L-1}
239 \|C_{0,\ell}\|
240 \|\Delta_\ell\|
241 \|C_{\ell+1,L}\|.
242 \]
243 \end{theorem}
244 
Proof block: Multilevel defect decomposition · Go to statement · Read statement and proof side by side245 \begin{proof}
246 Insert the intermediate terms
247 \[
248 C_{0,\ell}T_\ell C_{\ell,L}
249 \]
250 for $0\leq\ell\leq L$.  Consecutive differences telescope.  The difference between the terms indexed by $\ell+1$ and $\ell$ is
251 \[
252 C_{0,\ell}(C_\ell T_{\ell+1}-T_\ell C_\ell)C_{\ell+1,L}.
253 \]
254 Summing gives the identity.  The norm estimate follows from the triangle inequality.
255 \end{proof}
256 
257 \begin{interpretation}
258 The multilevel formula keeps track of where each mismatch enters. A defect at one level is composed with the comparison maps needed to reach the input and output levels. The norm estimate therefore depends on both the local defects and the maps that carry them through the hierarchy. Controlling local mismatches alone does not control the total error if those maps amplify them.
259 \end{interpretation}
260 
261 \begin{example}[A visible one step defect]\label{ex:defect_example}
262 Let $X_f=\bbk^2$, let $X_c=\bbk$, and let
263 \[
264 C(x_1,x_2)=x_1.
265 \]
266 Take
267 \[
268 T_f=
269 \begin{pmatrix}
270 a&b\\
271 c&d
272 \end{pmatrix},
273 \qquad
274 T_c=(a).
275 \]
276 Then
277 \[
278 \Delta=CT_f-T_cC=(0,b).
279 \]
280 The coarse operator is exactly compatible with the fine operator precisely when the discarded coordinate does not feed into the retained coordinate.  The entry $c$ does not appear in the one step defect because it moves information in the opposite direction.  It can still affect later powers through the terms in \cref{thm:power_defect}.
281 \end{example}
282 
Statement: Exact compatibility · Go to proof · Read statement and proof side by side283 \begin{corollary}[Exact compatibility]\label{cor:exact_compatibility}
284 If every one step defect $\Delta_\ell$ vanishes, then
285 \[
286 C_{0,L}p(T_L)=p(T_0)C_{0,L}
287 \]
288 for every polynomial $p$.  The analogous resolvent, holomorphic, and exponential identities also hold whenever the relevant expressions are defined.
289 \end{corollary}
290 
Proof block: Exact compatibility · Go to statement · Read statement and proof side by side291 \begin{proof}
292 The total one step defect vanishes by \cref{thm:multilevel_defect}.  Apply \cref{cor:polynomial_defect,thm:resolvent_defect,thm:holomorphic_defect,thm:exponential_defect}.
293 \end{proof}
294 

Back to source controls

Other PDFs for this work

Original file and source record

This copy matches the recorded source file. Its publication here does not change the work’s review status.

SHA-256: c39b31118fd60490e9ba19070a2ba8bfb45857ce80ac37a3f5b8a61ca068e79f

Original source on GitHub

Back to Paper II: Refinement Towers, Weighted Transfer, and Integral Separation of Operator Packets