OAI/Analysis/PureInfiniteness/CutMatrixDiagonalization.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Fixed spectral cuts in finite matrix diagonalization. The bound depends on the cut, but not on the two approximation tolerances or matrix size. This is the form of KR02 Lemmas 5.6 and 5.13 used in spectral localization.

  1. theorem OAI.WeakPureInfiniteness.finite_matrix_cut_diagonalization line 19