OAI/Geometry/Perimeter/Regularity/GeometricHausdorff.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RPISingularHarnack.geometricHausdorff line 12
  2. def OAI.RPISingularHarnack.hausdorffNormalizationRatio line 16
  3. theorem OAI.RPISingularHarnack.hausdorffNormalizationRatio_ne_zero line 21
  4. theorem OAI.RPISingularHarnack.hausdorffNormalizationRatio_ne_top line 31
  5. theorem OAI.RPISingularHarnack.geometricHausdorff_eq_smul_euclideanHausdorff line 39
  6. def OAI.RPISingularHarnack.boundaryArea line 47
  7. def OAI.RPISingularHarnack.WholeBoundarySobolev line 50
  8. def OAI.RPISingularHarnack.WholeBoundarySupersolution line 63
  9. def OAI.RPISingularHarnack.ZeroEssentialInfAtVertex line 69
  10. theorem OAI.RPI.Boundary.surfaceGradient_ae_eq_tangentialGradient line 84
  11. theorem OAI.RPISingularHarnack.boundaryArea_eq_smul_surfaceMeasure line 111
  12. theorem OAI.RPISingularHarnack.wholeBoundarySobolev_of_local_sobolevGraph line 118
  13. theorem OAI.RPISingularHarnack.eventually_filled_membership line 176
  14. theorem OAI.RPISingularHarnack.hasHalfspaceBlowup_of_regular_filled_chart line 205
  15. theorem OAI.RPISingularHarnack.hasHalfspaceBlowup_gradient_filled line 269
  16. theorem OAI.RPISingularHarnack.approximateNormal_eq_gradient_filled line 289
  17. def OAI.RPI.truncationSlope line 309
  18. def OAI.RPI.smoothTruncation line 311
  19. theorem OAI.RPI.truncationSlope_contDiff line 313
  20. theorem OAI.RPI.smoothTruncation_hasDerivAt line 317
  21. theorem OAI.RPI.smoothTruncation_deriv line 323
  22. theorem OAI.RPI.smoothTruncation_contDiff line 327
  23. theorem OAI.RPI.truncationSlope_mem_Icc line 332
  24. theorem OAI.RPI.truncationSlope_antitone line 335
  25. theorem OAI.RPI.smoothTruncation_second_deriv_nonpos line 340
  26. theorem OAI.RPI.smoothTruncation_zero line 345
  27. theorem OAI.RPI.smoothTruncation_monotone line 348
  28. theorem OAI.RPI.smoothTruncation_nonneg line 355
  29. theorem OAI.RPI.smoothTruncation_le_self line 359
  30. theorem OAI.RPI.truncationSlope_eq_zero line 367
  31. theorem OAI.RPI.truncationSlope_eq_one line 372
  32. theorem OAI.RPI.smoothTruncation_eq_self line 378
  33. theorem OAI.RPI.smoothTruncation_eq_at_one line 388
  34. theorem OAI.RPI.smoothTruncation_le_min line 406
  35. theorem OAI.RPI.min_sub_le_smoothTruncation line 414
  36. def OAI.RPI.truncationParameter line 426
  37. theorem OAI.RPI.truncationParameter_pos line 428
  38. theorem OAI.RPI.truncationParameter_le_one line 432
  39. theorem OAI.RPI.truncationParameter_tendsto line 438
  40. theorem OAI.RPI.smoothTruncation_tendsto line 441
  41. theorem OAI.RPI.truncationSlope_tendsto line 452