OAI/Geometry/Perimeter/Regularity/PerimeterAdmissiblePartitionPiece.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RPISingularHarnack.perimeterAdmissible_partition_piece line 14
  2. theorem OAI.RPISingularHarnack.divergence_finset_sum line 30
  3. theorem OAI.RPISingularHarnack.perimeter_iUnion_open_le line 45
  4. theorem OAI.RPISingularHarnack.raw_perimeter_empty_region line 106
  5. def OAI.RPISingularHarnack.openPerimeterCost line 116
  6. theorem OAI.RPISingularHarnack.openPerimeterCost_empty line 119
  7. def OAI.RPISingularHarnack.perimeterOuterMeasure line 123
  8. theorem OAI.RPISingularHarnack.perimeterOuterMeasure_le_open line 127
  9. theorem OAI.RPISingularHarnack.perimeterOuterMeasure_eq_iInf_open line 133
  10. theorem OAI.RPISingularHarnack.perimeterOuterMeasure_open line 154
  11. theorem OAI.RPISingularHarnack.separated_open_neighborhoods line 173
  12. theorem OAI.RPISingularHarnack.perimeterOuterMeasure_isMetric line 190
  13. def OAI.RPISingularHarnack.perimeterMeasure line 207
  14. theorem OAI.RPISingularHarnack.perimeterMeasure_open line 210
  15. theorem OAI.RPISingularHarnack.perimeterMeasure_support line 215
  16. theorem OAI.RPISingularHarnack.perimeterMeasure_locallyFinite line 242
  17. theorem OAI.RPISingularHarnack.perimeterMeasure_finiteOnCompacts line 251
  18. theorem OAI.RPISingularHarnack.measure_le_hausdorff_of_ball_growth line 269
  19. theorem OAI.RPISingularHarnack.exists_perimeter_vitali_cover_open line 325
  20. theorem OAI.RPISingularHarnack.hausdorffMeasure_inter_open_le_perimeter line 386
  21. theorem OAI.RPISingularHarnack.hausdorff_restrict_le_perimeterMeasure line 450
  22. theorem OAI.RPISingularHarnack.minimizing_perimeter_hausdorff_comparison line 493
  23. theorem OAI.RPISingularHarnack.minimizing_perimeter_hausdorff_mutuallyAC line 523