OAI/Geometry/Perimeter/Regularity/PerimeterEqOfAe.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RPISingularHarnack.perimeter_eq_of_ae line 13
  2. theorem OAI.RPISingularHarnack.perimeterSupport_eq_of_ae line 18
  3. theorem OAI.RPISingularHarnack.hasHalfspaceBlowup_iff_of_ae line 23
  4. theorem OAI.RPISingularHarnack.approximateNormal_eq_of_ae line 45
  5. theorem OAI.RPISingularHarnack.tangentialGradient_eq_of_ae line 52
  6. theorem OAI.RPISingularHarnack.boundaryArea_eq_of_ae line 58
  7. theorem OAI.RPISingularHarnack.wholeBoundarySobolev_iff_of_ae line 62
  8. theorem OAI.RPISingularHarnack.wholeBoundarySupersolution_iff_of_ae line 67
  9. theorem OAI.RPISingularHarnack.zeroEssentialInfAtVertex_iff_of_ae line 72
  10. theorem OAI.RPISingularHarnack.IsLocallyPerimeterMinimizing.of_ae line 89
  11. theorem OAI.RPISingularHarnack.tsupport_divergence_subset line 144
  12. theorem OAI.RPISingularHarnack.continuous_divergence line 154
  13. theorem OAI.RPISingularHarnack.integrable_divergence line 161
  14. theorem OAI.RPISingularHarnack.divergence_add line 167
  15. theorem OAI.RPISingularHarnack.raw_perimeter_mono_region line 174
  16. def OAI.RPISingularHarnack.PerimeterAdmissible line 181
  17. theorem OAI.RPISingularHarnack.perimeterAdmissible_zero line 184
  18. theorem OAI.RPISingularHarnack.perimeter_eq_iSup_tests line 188
  19. theorem OAI.RPISingularHarnack.perimeter_disjoint_superadditive line 193
  20. theorem OAI.RPISingularHarnack.divergence_smul line 230
  21. theorem OAI.RPISingularHarnack.smoothTransition_deriv_zero_of_nonpos line 242
  22. theorem OAI.RPISingularHarnack.smoothTransition_deriv_zero_of_one_le line 250
  23. theorem OAI.RPISingularHarnack.exists_smoothTransition_deriv_bound line 258
  24. def OAI.RPISingularHarnack.annularCutoff line 286
  25. theorem OAI.RPISingularHarnack.annularCutoff_contDiff line 289
  26. theorem OAI.RPISingularHarnack.annularCutoff_mem_Icc line 294
  27. theorem OAI.RPISingularHarnack.annularCutoff_zero line 298
  28. theorem OAI.RPISingularHarnack.annularCutoff_one line 307
  29. theorem OAI.RPISingularHarnack.tsupport_annularCutoff_subset line 315
  30. theorem OAI.RPISingularHarnack.gradient_annularCutoff line 323
  31. theorem OAI.RPISingularHarnack.gradient_annularCutoff_zero line 349
  32. theorem OAI.RPISingularHarnack.gradient_annularCutoff_bound line 364
  33. theorem OAI.RPISingularHarnack.volume_real_annulus line 394
  34. theorem OAI.RPISingularHarnack.gradient_annularCutoff_continuous line 405
  35. theorem OAI.RPISingularHarnack.gradient_annularCutoff_compact line 410
  36. theorem OAI.RPISingularHarnack.integral_gradient_annularCutoff_le line 420