OAI/Geometry/Perimeter/Regularity/AnnularCutoffTestAdmissible.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RPISingularHarnack.annularCutoff_test_admissible line 13
  2. theorem OAI.RPISingularHarnack.integral_annularCutoff_divergence_le line 33
  3. theorem OAI.RPISingularHarnack.annularCutoff_tendsto line 93
  4. theorem OAI.RPISingularHarnack.integral_divergence_outside_le line 116
  5. theorem OAI.RPISingularHarnack.perimeter_remove_closedBall_le line 171
  6. theorem OAI.RPISingularHarnack.locallyMinimizing_perimeter_growth line 186
  7. theorem OAI.RPISingularHarnack.exists_locallyMinimizing_perimeter_growth_constant line 220
  8. def OAI.RPISingularHarnack.radialNormalTest line 252
  9. def OAI.RPISingularHarnack.radialFlux line 255
  10. theorem OAI.RPISingularHarnack.radialNormalTest_contDiff line 258
  11. theorem OAI.RPISingularHarnack.radialNormalTest_support line 264
  12. theorem OAI.RPISingularHarnack.radialNormalTest_admissible line 274
  13. theorem OAI.RPISingularHarnack.divergence_radialNormalTest line 285
  14. theorem OAI.RPISingularHarnack.radialFlux_eq_indicator line 310
  15. theorem OAI.RPISingularHarnack.radialFlux_nonneg line 320
  16. theorem OAI.RPISingularHarnack.radialFlux_continuous line 324
  17. theorem OAI.RPISingularHarnack.radialFlux_support line 331
  18. theorem OAI.RPISingularHarnack.radialFlux_integrable line 341
  19. theorem OAI.RPISingularHarnack.integral_radialFlux_pos line 358
  20. theorem OAI.RPISingularHarnack.continuous_integral_radialFlux line 382
  21. theorem OAI.RPISingularHarnack.exists_uniform_radialFlux_lower line 393
  22. def OAI.RPISingularHarnack.ballNormalTest line 416
  23. theorem OAI.RPISingularHarnack.ballNormalTest_contDiff line 419
  24. theorem OAI.RPISingularHarnack.ballNormalTest_support line 423
  25. theorem OAI.RPISingularHarnack.ballNormalTest_admissible line 436
  26. theorem OAI.RPISingularHarnack.divergence_ballNormalTest line 446
  27. theorem OAI.RPISingularHarnack.ballNormalTest_allIntegral line 459
  28. theorem OAI.RPISingularHarnack.ballNormalTest_normalized_integral line 485
  29. theorem OAI.RPISingularHarnack.ballNormalTest_integral line 506