Intertwining Defect Bounds

Abstract

The weighted and uniform norm estimates jointly quantify defect propagation.

Theorem 1.1 (Both propagation bounds hold).

$$\begin{gathered} \forall K:Type,X:Type,Y:Type,A,C,T,L,n, \\ \mathrm{NontriviallyNormedField}(K)\wedge \mathrm{SeminormedAddCommGroup}(X)\wedge \mathrm{NormedSpace}(K,X)\wedge \\ \mathrm{SeminormedAddCommGroup}(Y)\wedge \mathrm{NormedSpace}(K,Y)\wedge A\in \mathrm{ContinuousLinearMap}(K,Y,Y)\wedge \\ C\in \mathrm{ContinuousLinearMap}(K,X,Y)\wedge T\in \mathrm{ContinuousLinearMap}(K,X,X)\wedge L\in R\wedge n\in N\Rightarrow \\ \Vert C\cdot T^n-A^n\cdot C\Vert \le \sum _{j=0}^{n-1}\Vert A{\Vert }^{n-1-j}\cdot \Vert C\cdot T-A\cdot C\Vert \cdot \Vert T{\Vert }^j\wedge \\ \Vert A\Vert \le L\wedge \Vert T\Vert \le L\Rightarrow \Vert C\cdot T^n-A^n\cdot C\Vert \le n\cdot L^{n-1}\cdot \Vert C\cdot T-A\cdot C\Vert \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Observer/Approximation/IntertwiningDefectBounds.intertwining_defect_propagation_bounds (✓ std3). ∎

Source. Repository-derived.

Commentary.

The first conjunct is the weighted finite-sum estimate. The second states that uniform bounds on both evolution operators imply the linear-in-time estimate.

Both conjuncts apply the canonical declarations from the existing intertwining-defect family; this module introduces no new mathematical definition.

References

• Truth anchor: D5/S3/Observer/Approximation/IntertwiningDefectBounds.intertwining_defect_propagation_bounds
• Dependency: D5/S3/Observer/Approximation/IntertwiningDefectPropagation