OAI/Geometry/Perimeter/Regularity/ConeLinkSupport.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RPISingularHarnack.SphericalFrankel.minimizing_perimeter_singleton line 11
2. lemma OAI.RPISingularHarnack.SphericalFrankel.minimizing_support_nonzero_point line 22
3. lemma OAI.RPISingularHarnack.SphericalFrankel.annularWeight_pos line 33
4. lemma OAI.RPISingularHarnack.SphericalFrankel.cone_support_annular_point line 42
5. lemma OAI.RPISingularHarnack.SphericalFrankel.annularFrameMeasure_ne_zero line 52
6. lemma OAI.RPISingularHarnack.SphericalFrankel.annularLink_ne_zero line 78
7. lemma OAI.RPISingularHarnack.SphericalFrankel.annularLink_radial_support line 85