OAI/Analysis/WeakInfiniteness/NuclearCompression.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakPureInfiniteness.finiteColumn line 34
2. lemma OAI.WeakPureInfiniteness.finiteColumn_initial line 38
3. lemma OAI.WeakPureInfiniteness.finiteColumn_norm_sq line 41
4. lemma OAI.WeakPureInfiniteness.finiteColumn_norm line 46
5. lemma OAI.WeakPureInfiniteness.finiteColumn_sandwich line 51
6. lemma OAI.WeakPureInfiniteness.norm_finite_sandwich_le line 57
7. def OAI.WeakPureInfiniteness.finiteCompression line 74
8. lemma OAI.WeakPureInfiniteness.finiteCompression_norm_le line 76
9. lemma OAI.WeakPureInfiniteness.finiteCompression_commutator line 91
10. lemma OAI.WeakPureInfiniteness.finiteCompression_commutator_norm_le line 106