OAI/Geometry/CylinderCovering/Rational/DomainArea.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SlopeRational.DomainArea.box line 14
2. lemma OAI.SlopeRational.DomainArea.box_isCompact line 17
3. lemma OAI.SlopeRational.DomainArea.box_volume line 42
4. def OAI.SlopeRational.DomainArea.centralBand line 51
5. lemma OAI.SlopeRational.DomainArea.centralBand_isClosed line 54
6. lemma OAI.SlopeRational.DomainArea.centralBand_subset_box line 62
7. lemma OAI.SlopeRational.DomainArea.centralBand_isCompact line 71
8. lemma OAI.SlopeRational.DomainArea.triangle_height_integral line 77
9. lemma OAI.SlopeRational.DomainArea.centralBand_volume line 107
10. lemma OAI.SlopeRational.DomainArea.wing_volumes line 136
11. lemma OAI.SlopeRational.DomainArea.area_sandwich line 145
12. lemma OAI.SlopeRational.DomainArea.ceiling_coefficients_bounds line 170
13. lemma OAI.SlopeRational.DomainArea.ceilingPolynomial_continuous line 191
14. lemma OAI.SlopeRational.DomainArea.ceilingPolynomial_bounds line 195
15. lemma OAI.SlopeRational.DomainArea.labelDomain_horizontal_bound line 217
16. lemma OAI.SlopeRational.DomainArea.padding_integral line 223
17. theorem OAI.SlopeRational.DomainArea.labelDomain_area_remainder line 233
18. lemma OAI.SlopeRational.DomainArea.unperturbed_domain line 293
19. lemma OAI.SlopeRational.DomainArea.unperturbed_domain_area line 304
20. lemma OAI.SlopeRational.DomainArea.unperturbed_subset line 310
21. lemma OAI.SlopeRational.DomainArea.added_domain_area line 319
22. lemma OAI.SlopeRational.DomainArea.ceilingIntegral_le_half line 326
23. theorem OAI.SlopeRational.DomainArea.labelDomain_area_bounds line 340
24. theorem OAI.SlopeRational.DomainArea.labelDomain_area_remainder_quadratic line 352
25. lemma OAI.SlopeRational.DomainArea.quadratic_padding_small line 368
26. theorem OAI.SlopeRational.DomainArea.labelDomain_area_estimates_small line 380