OAI/Analysis/Commutator/SpectralCutoff.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Kadison.Polar.partialIsometry_of_nonneg line 18
2. lemma OAI.Kadison.Polar.mul_rightSupport_eq_zero_of_nonneg line 31
3. lemma OAI.Kadison.Polar.rightSupport_mul_eq_zero_of_nonneg line 44
4. lemma OAI.Kadison.Polar.posPart_mem line 51
5. def OAI.Kadison.Polar.halfCut line 57
6. lemma OAI.Kadison.Polar.isProjection_halfCut line 60
7. lemma OAI.Kadison.Polar.halfCut_mem line 63
8. lemma OAI.Kadison.Polar.halfCut_mul_shift line 68
9. lemma OAI.Kadison.Polar.halfCut_commute line 80
10. lemma OAI.Kadison.Polar.halfCut_rounding line 88