OAI/Geometry/Perimeter/Regularity/ExistsMinimizingBoundaryAreaGrowth.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RPISingularHarnack.exists_minimizing_boundaryArea_growth line 14
  2. theorem OAI.RPISingularHarnack.approximateNormal_norm_le_one line 39
  3. theorem OAI.RPISingularHarnack.tangentialGradient_norm_le_twice line 47
  4. theorem OAI.RPISingularHarnack.exists_raw_minimizing_frontier_capacity_sequence line 62
  5. theorem OAI.RPISingularHarnack.tendsto_normalized_monotone_of_dyadic line 107
  6. def OAI.RPISingularHarnack.rescaledHalfspaceError line 150
  7. theorem OAI.RPISingularHarnack.rescaledHalfspaceError_eq line 156
  8. theorem OAI.RPISingularHarnack.hasHalfspaceBlowup_iff_dyadic line 167
  9. theorem OAI.RPISingularHarnack.measurable_rescaledHalfspaceError line 213
  10. theorem OAI.RPISingularHarnack.measurableSet_halfspaceBlowup line 235
  11. theorem OAI.RPISingularHarnack.measurable_approximateNormal line 244
  12. theorem OAI.RPISingularHarnack.measurable_tangentialGradient line 326
  13. theorem OAI.RPISingularHarnack.minimizing_boundaryArea_ball_lt_top line 334
  14. theorem OAI.RPISingularHarnack.tangentialGradient_memLp_on_ball line 340
  15. theorem OAI.RPISingularHarnack.tangentialGradient_mul line 355
  16. theorem OAI.RPISingularHarnack.tangentialGradient_eq_zero_of_notMem_tsupport line 367
  17. theorem OAI.RPISingularHarnack.boundaryArea_zero_of_singular_dim line 372
  18. theorem OAI.RPISingularHarnack.wholeBoundarySupersolution_of_regular_tests line 378