OAI/Geometry/Perimeter/Regularity/ExistsLocalVariationExtension.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RPISingularHarnack.exists_local_variation_extension line 13
2. theorem OAI.RPISingularHarnack.local_l2_integral_norm_le line 55
3. theorem OAI.RPISingularHarnack.l2_polar_norm_le_one line 82
4. theorem OAI.RPISingularHarnack.exists_local_variation_polar line 135
5. theorem OAI.RPISingularHarnack.exists_local_unit_variation_polar line 187
6. theorem OAI.RPISingularHarnack.smooth_translation_lintegral_le line 247
7. theorem OAI.RPISingularHarnack.indicator_translation_lintegral_le line 303
8. theorem OAI.RPISingularHarnack.c1Mollify_indicator_lintegral_error_le line 357
9. theorem OAI.RPISingularHarnack.c1Mollify_indicator_mem_Icc line 451
10. theorem OAI.RPISingularHarnack.c1Mollify_indicator_uniform_lipschitz line 479