OAI/Analysis/PlanarPacking/Schur.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SharpPlanar.neumann_exists_unique line 13
2. theorem OAI.SharpPlanar.neumann_norm_bound line 25
3. theorem OAI.SharpPlanar.schur_exists_unique line 43
4. theorem OAI.SharpPlanar.finite_schur_small line 77
5. theorem OAI.SharpPlanar.finite_schur_bound line 89
6. theorem OAI.SharpPlanar.tail_schur_small line 113
7. theorem OAI.SharpPlanar.tail_schur_bound line 129