OAI/Geometry/Perimeter/Regularity/GradientContDiff.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RPISingularHarnack.gradient_contDiff line 15
  2. theorem OAI.RPISingularHarnack.gradient_hasCompactSupport line 20
  3. theorem OAI.RPISingularHarnack.integral_mul_divergence_eq_neg_inner_gradient line 24
  4. def OAI.RPISingularHarnack.gradientDualTest line 70
  5. theorem OAI.RPISingularHarnack.gradientDualTest_contDiff line 73
  6. theorem OAI.RPISingularHarnack.gradientDualTest_hasCompactSupport line 82
  7. theorem OAI.RPISingularHarnack.gradientDualTest_norm_le line 87
  8. theorem OAI.RPISingularHarnack.integral_norm_gradient_le_of_test_bound line 99
  9. theorem OAI.RPISingularHarnack.indicator_one_integrable_compact line 177
  10. theorem OAI.RPISingularHarnack.c1Mollify_indicator_gradient_le_perimeter line 190
  11. theorem OAI.RPISingularHarnack.raw_perimeter_isoperimetric line 224
  12. theorem OAI.RPISingularHarnack.radial_volume_increment_le line 287
  13. theorem OAI.RPISingularHarnack.radial_volume_abs_sub_le line 303
  14. theorem OAI.RPISingularHarnack.radial_volume_continuousAt line 320
  15. theorem OAI.RPISingularHarnack.exists_controlled_cut_radius line 332
  16. theorem OAI.RPISingularHarnack.integral_gradient_annularCutoff_in_set_le line 370
  17. theorem OAI.RPISingularHarnack.controlled_radius_gradient_bound line 396