OAI/Geometry/Perimeter/Regularity/ExistsMinimizingDensityLimit.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RPISingularHarnack.exists_minimizing_density_limit line 18
  2. theorem OAI.RPISingularHarnack.minimizing_blowup_ball_real line 41
  3. theorem OAI.RPISingularHarnack.minimizing_dense_null_spheres line 59
  4. theorem OAI.RPISingularHarnack.minimizing_density_eq_of_null_spheres line 71
  5. theorem OAI.RPISingularHarnack.minimizing_density_limit_pos line 105
  6. theorem OAI.RPISingularHarnack.minimizing_blowup_limit_constant_density line 118
  7. theorem OAI.RPISingularHarnack.minimizing_tangent_cone_subsequence line 147
  8. theorem OAI.RPISingularHarnack.ae_subset_of_local_L1_limits line 215
  9. theorem OAI.RPISingularHarnack.canonical_subset_of_ae line 252
  10. theorem OAI.RPISingularHarnack.nested_minimizing_tangent_cones line 274
  11. theorem OAI.RPISingularHarnack.minimizing_support_limit_of_local_L1 line 334
  12. theorem OAI.RPISingularHarnack.minimizing_support_eventually_hits_of_local_L1 line 368
  13. theorem OAI.RPISingularHarnack.minimizing_supports_locally_converge line 402
  14. theorem OAI.RPISingularHarnack.perimeterSupport_blownUpSet line 469
  15. theorem OAI.RPISingularHarnack.cone_blowup_support_affine_mem line 483
  16. theorem OAI.RPISingularHarnack.minimizing_cone_tangent_support_line_invariant line 493