OAI/Geometry/Perimeter/Regularity/BlowupHomeomorph.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RPISingularHarnack.blowupHomeomorph line 18
  2. theorem OAI.RPISingularHarnack.blowupHomeomorph_apply line 21
  3. theorem OAI.RPISingularHarnack.blowupHomeomorph_symm_apply line 24
  4. theorem OAI.RPISingularHarnack.admissible_comp_blowup line 30
  5. theorem OAI.RPISingularHarnack.admissible_comp_blowdown line 38
  6. theorem OAI.RPISingularHarnack.divergence_comp_blowup line 51
  7. theorem OAI.RPISingularHarnack.integral_divergence_comp_blowup line 61
  8. theorem OAI.RPISingularHarnack.integral_divergence_comp_blowdown line 70
  9. theorem OAI.RPISingularHarnack.perimeter_blownUpSet_eq line 86
  10. theorem OAI.RPISingularHarnack.blownUpSet_ball line 107
  11. theorem OAI.RPISingularHarnack.locally_minimizing_blownUpSet line 113
  12. theorem OAI.RPISingularHarnack.exists_uniform_minimizing_exhaustion_cut line 173
  13. theorem OAI.RPISingularHarnack.exists_set_of_indicator_Lp line 203
  14. theorem OAI.RPISingularHarnack.exists_simultaneous_indicator_L1_subsequence line 226
  15. theorem OAI.RPISingularHarnack.exists_global_set_of_local_L1_limits line 270
  16. theorem OAI.RPISingularHarnack.minimizing_global_compactness line 337