OAI/Geometry/CylinderCovering/Singular/Cutoff.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CylinderCovering.SingularCutoff.tendsto_rpow_zero line 9
2. lemma OAI.CylinderCovering.SingularCutoff.rpow_isLittleO_rpow line 15
3. lemma OAI.CylinderCovering.SingularCutoff.powerCutoff_littleO line 24
4. lemma OAI.CylinderCovering.SingularCutoff.powerCutoff_derivative_small line 32
5. lemma OAI.CylinderCovering.SingularCutoff.powerPadding_littleO_square line 46
6. lemma OAI.CylinderCovering.SingularCutoff.cube_littleO_powerPadding line 56
7. theorem OAI.CylinderCovering.SingularCutoff.power_admissible line 68
8. theorem OAI.CylinderCovering.SingularCutoff.edge_one_alternative_admissible line 77
9. lemma OAI.CylinderCovering.SingularCutoff.cutoff_tendsto_zero line 84
10. lemma OAI.CylinderCovering.SingularCutoff.padding_tendsto_zero line 88
11. lemma OAI.CylinderCovering.SingularCutoff.tip_area_littleO line 94
12. lemma OAI.CylinderCovering.SingularCutoff.overlap_error_eventually line 98
13. lemma OAI.CylinderCovering.SingularCutoff.edge_one_coefficient_identity line 111
14. lemma OAI.CylinderCovering.SingularCutoff.edge_one_coefficient_negative line 117
15. lemma OAI.CylinderCovering.SingularCutoff.boundaryCoefficient_one line 124
16. lemma OAI.CylinderCovering.SingularCutoff.energyCoefficient_one line 127
17. lemma OAI.CylinderCovering.SingularCutoff.edgeOneCoefficient_one line 130