OAI/Combinatorics/TriangleRemoval/Spectral/StarInclusion.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpTerminalLeave.starInclusion line 21
2. def OAI.SharpTerminalLeave.extendStar line 24
3. theorem OAI.SharpTerminalLeave.starInclusion_mulVec line 27
4. theorem OAI.SharpTerminalLeave.extendStar_quadratic line 32
5. theorem OAI.SharpTerminalLeave.matrix_quadratic_abs line 41
6. theorem OAI.SharpTerminalLeave.hermitian_norm_le_of_quadratic line 58
7. theorem OAI.SharpTerminalLeave.sum_star_norm_bound line 75