OAI/Analysis/Commutator/CornerPolarTransfer.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Kadison.CornerPolarTransfer.conjugation_difference line 28
2. lemma OAI.Kadison.CornerPolarTransfer.range_compression line 56
3. lemma OAI.Kadison.CornerPolarTransfer.defect_bound line 66
4. lemma OAI.Kadison.CornerPolarTransfer.trace_kernel_bound line 72
5. lemma OAI.Kadison.CornerPolarTransfer.compressed_scalar_polar line 80
6. lemma OAI.Kadison.CornerPolarTransfer.scaled_projection_defect line 97
7. lemma OAI.Kadison.CornerPolarTransfer.norm_scaled_projection_defect line 111
8. lemma OAI.Kadison.CornerPolarTransfer.abs_coe line 126
9. lemma OAI.Kadison.CornerPolarTransfer.projection_of_coe line 131
10. theorem OAI.Kadison.CornerPolarTransfer.exists_polar_data line 135