OAI/Geometry/Perimeter/Regularity/TsupportBlowdownSubsetBall.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RPISingularHarnack.tsupport_blowdown_subset_ball line 15
  2. theorem OAI.RPISingularHarnack.tsupport_directionalDeriv_subset line 29
  3. theorem OAI.RPISingularHarnack.setIntegral_eq_of_inter_eq line 37
  4. theorem OAI.RPISingularHarnack.polar_blowup_test_error_le line 54
  5. theorem OAI.RPISingularHarnack.tendsto_doubled_polar_oscillation line 86
  6. theorem OAI.RPISingularHarnack.flat_distribution_of_polar_blowup_limit line 118
  7. theorem OAI.RPISingularHarnack.volumeReal_blownUpSet_closedBall line 212
  8. theorem OAI.RPISingularHarnack.indicator_L1_compl line 232
  9. theorem OAI.RPISingularHarnack.tendsto_volumeReal_inter_closedBall_of_indicator_L1 line 239
  10. theorem OAI.RPISingularHarnack.two_phase_of_indicator_L1 line 258
  11. theorem OAI.RPISingularHarnack.tendsto_rescaledHalfspaceError_of_indicator_L1 line 305
  12. theorem OAI.RPISingularHarnack.tendsto_of_every_subseq_has_subseq line 354
  13. theorem OAI.RPISingularHarnack.inter_eq_on_subdomain line 385
  14. theorem OAI.RPISingularHarnack.compl_inter_eq_of_inter_eq line 393
  15. theorem OAI.RPISingularHarnack.scaled_two_phase_bound_for_blownUpSet line 400
  16. theorem OAI.RPISingularHarnack.exists_halfspace_blowup_subsequence line 419
  17. theorem OAI.RPISingularHarnack.hasHalfspaceBlowup_of_differentiating_polar line 474