OAI/Analysis/Commutator/SpectralThreshold.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Kadison.PositiveWOT.positive_apply_eq_zero line 22
2. lemma OAI.Kadison.PositiveWOT.rightSupport_mono line 29
3. lemma OAI.Kadison.PositiveWOT.cfc_shift_posPart line 47
4. def OAI.Kadison.PositiveWOT.threshold line 57
5. lemma OAI.Kadison.PositiveWOT.threshold_projection line 60
6. lemma OAI.Kadison.PositiveWOT.threshold_mem line 63
7. lemma OAI.Kadison.PositiveWOT.threshold_antitone line 72
8. lemma OAI.Kadison.PositiveWOT.threshold_commute line 82
9. lemma OAI.Kadison.PositiveWOT.threshold_mul_shift line 93