OAI/Analysis/WeakInfiniteness/PerturbationRows.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakPureInfiniteness.diagonal_singleton line 36
2. lemma OAI.WeakPureInfiniteness.singleton_diagonal line 45
3. lemma OAI.WeakPureInfiniteness.norm_diagonalCopies_le line 47
4. lemma OAI.WeakPureInfiniteness.norm_row_test_le line 50
5. lemma OAI.WeakPureInfiniteness.rectangular_mul_sub_perturb line 63
6. lemma OAI.WeakPureInfiniteness.rectangular_sub_mul_perturb line 68
7. lemma OAI.WeakPureInfiniteness.rectangular_neg_mul_perturb line 73
8. lemma OAI.WeakPureInfiniteness.rectangular_mul_neg_perturb line 77
9. lemma OAI.WeakPureInfiniteness.compress_row_test line 81
10. lemma OAI.WeakPureInfiniteness.norm_representation_compression_le line 94
11. lemma OAI.WeakPureInfiniteness.supported_testing_element line 117