OAI/Geometry/Perimeter/Regularity/IntegralDivergenceEqZero.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RPISingularHarnack.integral_divergence_eq_zero line 13
  2. theorem OAI.RPISingularHarnack.divergence_neg line 47
  3. theorem OAI.RPISingularHarnack.perimeterAdmissible_neg line 53
  4. theorem OAI.RPISingularHarnack.raw_perimeter_compl_le line 58
  5. theorem OAI.RPISingularHarnack.raw_perimeter_compl line 70
  6. theorem OAI.RPISingularHarnack.perimeterSupport_compl line 75
  7. theorem OAI.RPISingularHarnack.isLocallyPerimeterMinimizing_compl line 80
  8. theorem OAI.RPISingularHarnack.raw_perimeter_eq_zero_of_volume_inter_eq_zero line 95
  9. theorem OAI.RPISingularHarnack.minimizing_two_phase_volume_lower line 113
  10. theorem OAI.RPISingularHarnack.holder_volume_scale line 147
  11. theorem OAI.RPISingularHarnack.minimizing_scaled_clearing_out line 152
  12. theorem OAI.RPISingularHarnack.minimizing_scaled_two_phase_volume_lower line 222
  13. theorem OAI.RPISingularHarnack.indicator_one_locallyIntegrable line 257
  14. theorem OAI.RPISingularHarnack.average_indicator_one_closedBall line 264
  15. theorem OAI.RPISingularHarnack.minimizing_phaseSupport_volume_lower line 272
  16. theorem OAI.RPISingularHarnack.minimizing_ae_eq_phaseSupport line 288