OAI/Geometry/CylinderCovering/Rational/CostExpansion.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CylinderCovering.RationalCost.integral_weight_remainder line 12
2. theorem OAI.CylinderCovering.RationalCost.changing_domain_remainder line 54
3. theorem OAI.CylinderCovering.RationalCost.cost_expansion_bound line 85
4. theorem OAI.CylinderCovering.RationalCost.cost_expansion_bound_of_area line 109