OAI/Geometry/Perimeter/Regularity/TendstoWeightedHalfspaceBlowup.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RPISingularHarnack.tendsto_weighted_halfspaceBlowup line 14
2. theorem OAI.RPISingularHarnack.exists_halfspace_perimeter_lower_density_constant line 86
3. theorem OAI.RPISingularHarnack.perimeter_finset_disjoint_superadditive line 124
4. theorem OAI.RPISingularHarnack.perimeter_tsum_disjoint_le line 148
5. theorem OAI.RPISingularHarnack.exists_perimeter_vitali_cover line 170
6. theorem OAI.RPISingularHarnack.hausdorffMeasure_le_perimeter_of_lower_density line 247
7. theorem OAI.RPISingularHarnack.exists_minimizing_surfaceMeasure_growth_of_halfspace line 312
8. theorem OAI.RPISingularHarnack.min_wholeBoundarySobolev_and_supersolution_of_minimizing_regular_geometry line 390
9. def OAI.RPI.Boundary.c1Mollifier line 437
10. def OAI.RPI.Boundary.c1Mollify line 441
11. lemma OAI.RPI.Boundary.c1Mollifier_radius_tendsto line 444
12. lemma OAI.RPI.Boundary.c1Mollify_contDiff line 448
13. lemma OAI.RPI.Boundary.c1Mollify_hasCompactSupport line 453
14. lemma OAI.RPI.Boundary.c1Mollify_fderiv line 457
15. lemma OAI.RPI.Boundary.c1Mollify_tendsto line 469
16. lemma OAI.RPI.Boundary.c1Mollify_fderiv_tendsto line 473
17. lemma OAI.RPI.Boundary.c1Mollify_nonneg line 480
18. lemma OAI.RPI.Boundary.c1Mollify_uniform_bound line 486
19. lemma OAI.RPI.Boundary.c1Mollify_tsupport_subset line 528
20. lemma OAI.RPI.Boundary.c1Mollify_eventually_tsupport_subset line 537