OAI/Analysis/JiangSu/CStarAlgebras/FourEdgeConjugationEstimates.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FourEdgeSurgery.logarithmicFlow line 17
2. lemma OAI.FourEdgeSurgery.conjugation_one line 22
3. lemma OAI.FourEdgeSurgery.conjugation_mul line 25
4. lemma OAI.FourEdgeSurgery.conjugation_inv_cancel line 29
5. lemma OAI.FourEdgeSurgery.conjugation_inv_cancel' line 32
6. lemma OAI.FourEdgeSurgery.conjugation_distance line 36
7. lemma OAI.FourEdgeSurgery.conjugation_comp_error line 41
8. lemma OAI.FourEdgeSurgery.conjugation_change_test line 48
9. lemma OAI.FourEdgeSurgery.conjugated_unitary_error line 57
10. lemma OAI.FourEdgeSurgery.correction_error line 68
11. theorem OAI.FourEdgeSurgery.surgery_control line 96