OAI/Geometry/Perimeter/Regularity/SmoothFlatOrder.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RPISingularHarnack.smooth_flat_order line 14
  2. theorem OAI.RPISingularHarnack.indicator_convolution_fderiv_eq line 65
  3. theorem OAI.RPISingularHarnack.halfspace_of_flat_distribution line 91
  4. theorem OAI.RPISingularHarnack.halfspace_threshold_eq_zero line 186
  5. def OAI.RPISingularHarnack.blownUpSet line 243
  6. theorem OAI.RPISingularHarnack.measurableSet_blownUpSet line 246
  7. theorem OAI.RPISingularHarnack.integral_blownUpSet line 250
  8. theorem OAI.RPISingularHarnack.divergence_comp_blowdown line 262
  9. theorem OAI.RPISingularHarnack.perimeter_blownUpSet_le line 273
  10. theorem OAI.RPISingularHarnack.exists_fixed_annular_bv_cut line 327
  11. theorem OAI.RPISingularHarnack.exists_local_indicator_L1_subsequence line 353
  12. theorem OAI.RPISingularHarnack.exists_blownUpSet_perimeter_bound line 395
  13. theorem OAI.RPISingularHarnack.divergence_scalar_direction line 432
  14. theorem OAI.RPISingularHarnack.integral_fderiv_blownUpSet line 440
  15. theorem OAI.RPISingularHarnack.integral_fderiv_blownUpSet_polar line 460
  16. theorem OAI.RPISingularHarnack.polar_test_oscillation_le line 480