OAI/Geometry/Perimeter/Regularity/FiberHeight.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RPISingularHarnack.minimizing_phase_constant_off_support line 11
2. theorem OAI.RPISingularHarnack.minimizing_phase_absent_of_anchor line 42
3. theorem OAI.RPISingularHarnack.minimizing_phase_present_of_anchor line 55
4. theorem OAI.RPISingularHarnack.minimizing_slab_phase_agreement line 68
5. def OAI.RPISingularHarnack.localizedPhaseError line 105
6. def OAI.RPISingularHarnack.fiberHeight line 109
7. theorem OAI.RPISingularHarnack.localizedPhaseError_measurable line 112
8. theorem OAI.RPISingularHarnack.localizedPhaseError_norm_le_one line 119
9. theorem OAI.RPISingularHarnack.fiberHeight_add_smul line 127
10. theorem OAI.RPISingularHarnack.fiberHeight_stronglyMeasurable line 139
11. theorem OAI.RPISingularHarnack.unit_inner_add_smul line 146
12. theorem OAI.RPISingularHarnack.ae_fiber_norm_bound line 151
13. theorem OAI.RPISingularHarnack.norm_fiber_integral_le line 175
14. theorem OAI.RPISingularHarnack.localizedPhaseError_slab_bound line 193
15. theorem OAI.RPISingularHarnack.fiberHeight_slab_bound line 215
16. theorem OAI.RPISingularHarnack.lintegral_fiber_bound line 223
17. theorem OAI.RPISingularHarnack.slab_lintegral_bound line 249
18. theorem OAI.RPISingularHarnack.slab_integral_bound line 296
19. def OAI.RPISingularHarnack.cutoffPhaseError line 310
20. theorem OAI.RPISingularHarnack.cutoffPhaseError_measurable line 314
21. theorem OAI.RPISingularHarnack.cutoffPhaseError_support line 320
22. theorem OAI.RPISingularHarnack.cutoffPhaseError_eq_mul_localized line 325
23. theorem OAI.RPISingularHarnack.cutoffPhaseError_slab_bound line 334