OAI/Geometry/Perimeter/Regularity/IndicatorConvolutionVariationLocalLe.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RPISingularHarnack.indicator_convolution_variation_local_le line 16
  2. theorem OAI.RPISingularHarnack.scalar_compact_integration_parts line 91
  3. theorem OAI.RPISingularHarnack.integral_mul_divergence_eq_neg_inner_gradient_local line 113
  4. theorem OAI.RPISingularHarnack.integral_weighted_norm_gradient_le_of_test_bound line 148
  5. theorem OAI.RPISingularHarnack.c1Mollify_indicator_local_gradient_le line 225
  6. theorem OAI.RPISingularHarnack.c1Mollify_indicator_norm_le_one line 288
  7. theorem OAI.RPISingularHarnack.raw_ball_poincare line 298
  8. theorem OAI.RPISingularHarnack.exists_minimizing_perimeter_lower_density line 387
  9. theorem OAI.RPISingularHarnack.exists_minimizing_surfaceMeasure_growth line 456