OAI/Geometry/Perimeter/Regularity/MollifiedFiberMoment.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RPISingularHarnack.phaseMollification_eq_one_of_ae line 13
2. theorem OAI.RPISingularHarnack.phaseMollification_eq_zero_of_ae line 27
3. theorem OAI.RPISingularHarnack.phaseMollification_lower_cap line 38
4. theorem OAI.RPISingularHarnack.phaseMollification_upper_cap line 63
5. def OAI.RPISingularHarnack.mollifiedNormalProfile line 89
6. theorem OAI.RPISingularHarnack.mollifiedNormalProfile_contDiff line 93
7. theorem OAI.RPISingularHarnack.mollifiedNormalProfile_deriv line 99
8. theorem OAI.RPISingularHarnack.mollifiedNormalProfile_flux_defect line 110