OAI/Geometry/CylinderCovering/Convexity/SpectralNormComparison.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SpectralNormComparison.offDiagonal_apply line 10
2. theorem OAI.SpectralNormComparison.offDiagonalLinear_apply line 13
3. theorem OAI.SpectralNormComparison.norm_sq line 16
4. theorem OAI.SpectralNormComparison.norm_offDiagonal line 19
5. theorem OAI.SpectralNormComparison.hasEigenvalue_conj line 44
6. theorem OAI.SpectralNormComparison.hasEigenvalue_conj_iff line 57
7. theorem OAI.SpectralNormComparison.square_zero_conj_iff line 67
8. theorem OAI.SpectralNormComparison.physicalScale_conj_offDiagonal line 73
9. theorem OAI.SpectralNormComparison.comparison_eigenvalues line 80
10. theorem OAI.SpectralNormComparison.comparison_norm line 101
11. theorem OAI.SpectralNormComparison.comparison_rescaled_norm line 105
12. theorem OAI.SpectralNormComparison.offDiagonal_square line 113
13. theorem OAI.SpectralNormComparison.eigenvalue_sq line 119
14. theorem OAI.SpectralNormComparison.comparison_spectrum line 132
15. theorem OAI.SpectralNormComparison.comparison_hyperbolic line 146
16. theorem OAI.SpectralNormComparison.comparison_not_orthogonal_bound line 154
17. theorem OAI.SpectralNormComparison.fderiv_physical_conjugate line 159
18. theorem OAI.SpectralNormComparison.physical_square_zero_iff line 175
19. theorem OAI.SpectralNormComparison.physical_eigenvalue_iff line 187