OAI/Analysis/WeakInfiniteness/CuntzPairCorrection.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakPureInfiniteness.rectangular_norm_le_sum_entries line 29
2. lemma OAI.WeakPureInfiniteness.exists_inverse_sqrt_tolerance line 43
3. lemma OAI.WeakPureInfiniteness.exists_rectangular_isometry_near line 66
4. def OAI.WeakPureInfiniteness.cuntzPairRow line 108
5. lemma OAI.WeakPureInfiniteness.cuntzPairRow_apply line 112
6. lemma OAI.WeakPureInfiniteness.cuntzPairRow_initial_entry line 116
7. lemma OAI.WeakPureInfiniteness.norm_cuntzPairRow_le line 122
8. lemma OAI.WeakPureInfiniteness.norm_cuntzPairRow_initial_sub_one_le line 126
9. lemma OAI.WeakPureInfiniteness.exists_cuntzPair_near line 139