OAI/Analysis/WeakInfiniteness/CentralizationEstimates.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakPureInfiniteness.norm_commutator_sq_le_unital line 28
2. lemma OAI.WeakPureInfiniteness.norm_commutator_sq_le line 64
3. lemma OAI.WeakPureInfiniteness.norm_relative_initial_defect_le line 72
4. lemma OAI.WeakPureInfiniteness.norm_relative_cross_defect_le line 82
5. def OAI.WeakPureInfiniteness.ContractiveIdentityDiagonalization line 92
6. def OAI.WeakPureInfiniteness.LocalCentralCuntzPair line 96
7. lemma OAI.WeakPureInfiniteness.ContractiveIdentityDiagonalization.localCentralCuntzPair line 101
8. lemma OAI.WeakPureInfiniteness.LocalCentralCuntzPair.contractiveIdentityDiagonalization line 143
9. lemma OAI.WeakPureInfiniteness.contractiveIdentityDiagonalization_iff_localCentralCuntzPair line 172