OAI/Geometry/Perimeter/Regularity/Space.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.RPI.Boundary.Space line 11
  2. def OAI.RPI.Boundary.divergence line 13
  3. def OAI.RPI.Boundary.PerimeterTest line 16
  4. def OAI.RPI.Boundary.perimeter line 19
  5. theorem OAI.RPI.Boundary.perimeter_mono line 23
  6. theorem OAI.RPI.Boundary.perimeter_congr_ae line 32
  7. def OAI.RPI.Boundary.LocallyFinitePerimeter line 37
  8. def OAI.RPI.Boundary.CompactVariationIn line 40
  9. def OAI.RPI.Boundary.LocallyPerimeterMinimizing line 44
  10. def OAI.RPI.Boundary.perimeterSupport line 49
  11. theorem OAI.RPI.Boundary.isClosed_perimeterSupport line 52
  12. def OAI.RPI.Boundary.IsCone line 72
  13. def OAI.RPI.Boundary.surfaceMeasure line 75
  14. theorem OAI.RPI.Boundary.surfaceMeasure_zero_of_dimH_lt line 78
  15. theorem OAI.RPI.Boundary.surfaceMeasure_zero_of_singular_dim line 87
  16. theorem OAI.RPI.Boundary.contact_measure_zero line 93
  17. def OAI.RPI.Boundary.tangentPlane line 109
  18. def OAI.RPI.Boundary.surfaceGradient line 114
  19. def OAI.RPI.Boundary.smoothGradientGraph line 118
  20. def OAI.RPI.Boundary.IsLocalSobolevPair line 126
  21. def OAI.RPI.Boundary.IsWeakLaplaceSupersolution line 133
  22. theorem OAI.RPI.Boundary.surfaceGradient_congr_trace line 151
  23. def OAI.RPI.Boundary.HasSmoothTraceAt line 186
  24. theorem OAI.RPI.Boundary.exists_contDiff_eqOn_of_local_trace line 191
  25. def OAI.RPI.Boundary.HasSmoothTraceJetAt line 223
  26. lemma OAI.RPI.Boundary.HasSmoothTraceJetAt.trace line 228
  27. theorem OAI.RPI.Boundary.surfaceGradient_mul line 234
  28. theorem OAI.RPI.Boundary.surfaceGradient_const line 247
  29. theorem OAI.RPI.Boundary.exists_smooth_cutoff_trace line 251