OAI/Geometry/CylinderCovering/Singular/Cost.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CylinderCovering.FlexibleSingular.labelDomain_volume_vertical line 10
2. def OAI.CylinderCovering.FlexibleSingular.capQuotient line 26
3. lemma OAI.CylinderCovering.FlexibleSingular.capQuotient_nonneg_bound line 30
4. lemma OAI.CylinderCovering.FlexibleSingular.capQuotient_inside line 42
5. lemma OAI.CylinderCovering.FlexibleSingular.ceiling_eventually line 53
6. lemma OAI.CylinderCovering.FlexibleSingular.capQuotient_tendsto line 67
7. lemma OAI.CylinderCovering.FlexibleSingular.capQuotient_integral_tendsto line 91
8. lemma OAI.CylinderCovering.FlexibleSingular.labelDomain_volume_difference line 122
9. lemma OAI.CylinderCovering.FlexibleSingular.labelDomain_volume_tendsto line 149
10. lemma OAI.CylinderCovering.FlexibleSingular.labelDomain_subset_cone line 163
11. lemma OAI.CylinderCovering.FlexibleSingular.labelDomain_eventually_mem line 167
12. lemma OAI.CylinderCovering.FlexibleSingular.flexibleEnergy_integral_tendsto line 190
13. lemma OAI.CylinderCovering.FlexibleSingular.flexibleEnergy_integrable line 241
14. lemma OAI.CylinderCovering.FlexibleSingular.weighted_integral_expansion line 247
15. lemma OAI.CylinderCovering.FlexibleSingular.weighted_integral_tendsto line 255
16. lemma OAI.CylinderCovering.FlexibleSingular.totalCost_quotient_tendsto line 274
17. lemma OAI.CylinderCovering.FlexibleSingular.asymptotic line 287
18. lemma OAI.CylinderCovering.FlexibleSingular.totalCost_small line 304
19. lemma OAI.CylinderCovering.FlexibleSingular.labelDomain_eq_upper_one line 315