OAI/Analysis/PlanarPacking/MatrixL1.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SharpPlanar.L1Finite line 11
2. def OAI.SharpPlanar.matrixL1 line 17
3. lemma OAI.SharpPlanar.matrixL1_apply line 20
4. lemma OAI.SharpPlanar.l1Finite_norm line 23
5. lemma OAI.SharpPlanar.matrixL1_mul line 27
6. lemma OAI.SharpPlanar.matrixL1_sub line 35
7. lemma OAI.SharpPlanar.matrixL1_one line 39
8. lemma OAI.SharpPlanar.matrixL1_norm_le line 44
9. lemma OAI.SharpPlanar.matrixL1_norm_lt line 59
10. lemma OAI.SharpPlanar.approximate_inverse_bijective line 70
11. lemma OAI.SharpPlanar.approximate_inverse_estimate line 84