OAI/Geometry/Perimeter/Regularity/C1MinRegularTest.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RPI.Boundary.c1_min_regular_test line 25
  2. theorem OAI.RPI.Boundary.c1_min_regular_energy line 62
  3. theorem OAI.RPI.Boundary.c1_min_local_energy line 120
  4. theorem OAI.RPISingularHarnack.c1_min_wholeBoundarySobolev_and_supersolution_of_regular_geometry line 227
  5. theorem OAI.RPISingularHarnack.c1_min_wholeBoundarySobolev_and_supersolution_of_minimizing_regular_geometry line 328
  6. theorem OAI.RPISingularHarnack.divergence_comp_add_right line 376
  7. theorem OAI.RPISingularHarnack.integral_divergence_le_perimeter_real line 383
  8. theorem OAI.RPISingularHarnack.indicator_convolution_variation_le line 390