OAI/Analysis/WeakInfiniteness/SpectralDeletion.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakPureInfiniteness.sqrt_mul_eq_zero_of_sandwich_eq_zero line 29
2. lemma OAI.WeakPureInfiniteness.eq_zero_of_nonneg_of_partition_diagonals line 45
3. lemma OAI.WeakPureInfiniteness.both_signs_of_partition_diagonals line 56
4. def OAI.WeakPureInfiniteness.finiteDeletion line 76
5. lemma OAI.WeakPureInfiniteness.finiteDeletion_selfAdjoint line 79
6. lemma OAI.WeakPureInfiniteness.finiteDeletion_diagonals line 95
7. lemma OAI.WeakPureInfiniteness.finiteDeletion_preserves_corner line 121