OAI/Probability/SignedSweeps/SpectralCommute.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SignedSweeps.symmetric_eq_basisDiagonal line 14
2. lemma OAI.SignedSweeps.diagonal_function_commute line 21
3. lemma OAI.SignedSweeps.basisDiagonal_function_commute line 39
4. lemma OAI.SignedSweeps.spectralFunction_commute line 50
5. lemma OAI.SignedSweeps.positiveRoot_commute line 57
6. lemma OAI.SignedSweeps.supportInverseRoot_commute line 61
7. lemma OAI.SignedSweeps.spectralSupport_commute line 65
8. lemma OAI.SignedSweeps.spectralSupport_root line 69
9. lemma OAI.SignedSweeps.positiveRoot_right_support line 76
10. theorem OAI.SignedSweeps.support_inverse_insertion line 97