OAI/Geometry/CylinderCovering/Singular/EdgeOneCost.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CylinderCovering.SingularEdgeOneCover.labelMap_image line 12
2. lemma OAI.CylinderCovering.SingularEdgeOneCover.cost_dictionary line 25
3. lemma OAI.CylinderCovering.SingularEdgeOneCover.cost_dictionary_eventually line 34
4. lemma OAI.CylinderCovering.SingularEdgeOneCover.cost_quotient_tendsto line 50
5. lemma OAI.CylinderCovering.SingularEdgeOneCover.cost_asymptotic line 67
6. lemma OAI.CylinderCovering.SingularEdgeOneCover.totalCost_small line 83
7. lemma OAI.CylinderCovering.SingularEdgeOneCover.finite_families_eventually line 94
8. theorem OAI.CylinderCovering.SingularEdgeOneCover.cost_statement line 126
9. theorem OAI.CylinderCovering.SingularEdgeOneCover.alternative_cost line 137