OAI/Geometry/Perimeter/Regularity/IntegralDivergenceEqZeroOfPerimeterEqZero.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RPISingularHarnack.integral_divergence_eq_zero_of_perimeter_eq_zero line 15
2. theorem OAI.RPISingularHarnack.convolution_fderiv_eq_zero_of_perimeter_eq_zero line 48
3. theorem OAI.RPISingularHarnack.volume_inter_eq_zero_or_compl_of_perimeter_eq_zero line 90
4. theorem OAI.RPISingularHarnack.perimeterSupport_eq_phaseSupport_inter line 149
5. theorem OAI.RPISingularHarnack.minimizing_frontier_phaseSupport line 180
6. theorem OAI.RPISingularHarnack.chord_half_norm_sub_le line 215
7. theorem OAI.RPISingularHarnack.chord_half_integral_le line 246
8. theorem OAI.RPISingularHarnack.integrated_chord_half_le line 282
9. theorem OAI.RPISingularHarnack.smooth_ball_poincare line 328