OAI/Geometry/Cannon/Boundary/WordBall.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CannonPaths.expansion_image_small line 13
2. theorem OAI.CannonRelease.boundary_controlled_regular_disks line 37
3. lemma OAI.CannonMetric.compact_packing_bound line 249
4. lemma OAI.CannonRelease.finite_triple_translates line 286
5. lemma OAI.CannonRelease.visual_ball_expansion line 299
6. theorem OAI.CannonRelease.relative_packing_bound line 327
7. def OAI.CannonGraph.wordBall line 373
8. lemma OAI.CannonGraph.one_mem_wordBall line 377
9. lemma OAI.CannonGraph.wordBall_step line 385
10. lemma OAI.CannonGraph.walk_end_mem_wordBall line 392
11. lemma OAI.CannonGraph.wordBall_card line 417
12. lemma OAI.CannonRelease.boundaryDist_le_of_prefix line 440
13. lemma OAI.CannonRelease.global_prefix_packing line 452
14. lemma OAI.CannonReal.power_counting_bound line 481
15. lemma OAI.CannonRelease.global_polynomial_packing line 516