OAI/Geometry/Perimeter/Regularity/WholeBoundarySublevelMeasureStep.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RPISingularHarnack.wholeBoundary_sublevel_measure_step line 17
  2. lemma OAI.RPIIteration.exists_small_power line 107
  3. theorem OAI.RPIIteration.superlinear_iteration line 127
  4. lemma OAI.RPIIteration.exists_small_positive_sublevel line 171
  5. def OAI.RPIIteration.radius line 214
  6. def OAI.RPIIteration.level line 215
  7. lemma OAI.RPIIteration.radius_bounds line 217
  8. lemma OAI.RPIIteration.radius_succ_lt line 222
  9. lemma OAI.RPIIteration.level_bounds line 227
  10. lemma OAI.RPIIteration.level_succ_lt line 238
  11. lemma OAI.RPIIteration.level_zero line 241
  12. lemma OAI.RPIIteration.quotient_bound line 243
  13. lemma OAI.RPIIteration.power_step line 266
  14. theorem OAI.RPISingularHarnack.no_positive_bounded_supersolution_with_zero_vertex_inf line 299
  15. theorem OAI.RPISingularHarnack.minimizing_boundaryArea_ball_pos line 386
  16. theorem OAI.RPISingularHarnack.regular_ball_nonempty line 398
  17. theorem OAI.RPISingularHarnack.zeroEssentialInf_of_median_small_infimum line 419
  18. theorem OAI.RPISingularHarnack.no_regular_positive_supersolution_with_median_bound line 481