OAI/Analysis/Commutator/IsometryCompression.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Kadison.FreeCorner.isometry_adjoint_apply line 21
2. lemma OAI.Kadison.FreeCorner.isometry_project_range line 26
3. def OAI.Kadison.FreeCorner.factorIsometry line 32
4. lemma OAI.Kadison.FreeCorner.factorIsometry_comp line 40
5. lemma OAI.Kadison.FreeCorner.compress_factorIsometry line 47
6. lemma OAI.Kadison.FreeCorner.norm_compress_le_of_range_subset line 54