OAI/Analysis/WeakInfiniteness/TensorCompression.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakPureInfiniteness.compress line 24
2. lemma OAI.WeakPureInfiniteness.norm_compress_le line 28
3. lemma OAI.WeakPureInfiniteness.norm_tensorSum_compress_le line 36
4. lemma OAI.WeakPureInfiniteness.norm_tensorSum_le_of_finite_compressions line 70
5. theorem OAI.WeakPureInfiniteness.tensor_norm_le_faithful line 117