OAI/Geometry/Perimeter/Regularity/SetIntegralSubLeSymmDiff.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RPISingularHarnack.setIntegral_sub_le_symmDiff line 17
  2. theorem OAI.RPISingularHarnack.integral_smooth_patch_le line 34
  3. def OAI.RPISingularHarnack.gluedFilledSet line 84
  4. theorem OAI.RPISingularHarnack.controlled_radius_glued_perimeter_le line 87
  5. theorem OAI.RPISingularHarnack.minimizing_controlled_replacement_perimeter_le line 142
  6. theorem OAI.RPISingularHarnack.exists_controlled_annular_cut_radius line 188
  7. theorem OAI.RPISingularHarnack.minimizing_annular_replacement_perimeter_le line 218
  8. theorem OAI.RPISingularHarnack.eventually_minimizing_perimeter_le_of_annular_L1 line 231
  9. theorem OAI.RPISingularHarnack.lintegral_indicator_difference line 250
  10. theorem OAI.RPISingularHarnack.abs_setIntegral_sub_le_symmDiff_volume line 262
  11. theorem OAI.RPISingularHarnack.tendsto_setIntegral_of_local_symmDiff line 286
  12. theorem OAI.RPISingularHarnack.perimeter_le_of_eventually_le_of_local_L1 line 310
  13. theorem OAI.RPISingularHarnack.locally_minimizing_of_local_L1_limit line 329
  14. theorem OAI.RPISingularHarnack.tendsto_perimeter_ball_right line 386
  15. theorem OAI.RPISingularHarnack.tendsto_minimizing_perimeter_ball_of_local_L1 line 400