OAI/Geometry/Perimeter/Regularity/ContinuousWithinAtSurfaceGradientOfLocalLevel.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RPI.Boundary.continuousWithinAt_surfaceGradient_of_local_level line 11
  2. theorem OAI.RPI.Boundary.surfaceGradient_aestronglyMeasurable_of_regular_locus line 51
  3. theorem OAI.RPI.Boundary.exists_geometric_capacity_sequence line 85
  4. theorem OAI.RPI.vectorEnergy_sub_tendsto_zero_of_toLp_tendsto line 120
  5. theorem OAI.RPI.Boundary.exists_compact_energy_approximants_of_mem_sobolevGraph line 136
  6. abbrev OAI.RPISingularHarnack.Euc line 167
  7. def OAI.RPISingularHarnack.HasHalfspaceBlowup line 169
  8. def OAI.RPISingularHarnack.approximateNormal line 177
  9. def OAI.RPISingularHarnack.tangentialGradient line 181
  10. theorem OAI.RPISingularHarnack.eventually_sublevel_membership line 186
  11. theorem OAI.RPISingularHarnack.normalized_ball_integral line 213
  12. theorem OAI.RPISingularHarnack.ae_linear_ne_zero line 233
  13. theorem OAI.RPISingularHarnack.halfspace_indicator_rescale line 245
  14. theorem OAI.RPISingularHarnack.hasHalfspaceBlowup_of_regular_sublevel line 253
  15. theorem OAI.RPISingularHarnack.hasHalfspaceBlowup_gradient line 317
  16. theorem OAI.RPISingularHarnack.halfspace_wedge_nonempty line 337
  17. theorem OAI.RPISingularHarnack.eq_of_halfspace_indicator_ae line 358
  18. theorem OAI.RPISingularHarnack.integrable_rescaled_indicator line 379
  19. theorem OAI.RPISingularHarnack.HasHalfspaceBlowup.tendstoInMeasure line 392
  20. theorem OAI.RPISingularHarnack.HasHalfspaceBlowup.unique line 425
  21. theorem OAI.RPISingularHarnack.approximateNormal_eq_of_blowup line 431
  22. theorem OAI.RPISingularHarnack.approximateNormal_eq_gradient line 437
  23. theorem OAI.RPI.Boundary.surfaceGradient_eq_tangentialGradient line 455
  24. def OAI.RPISingularHarnack.divergence line 485
  25. def OAI.RPISingularHarnack.perimeter line 489
  26. def OAI.RPISingularHarnack.perimeterSupport line 494
  27. def OAI.RPISingularHarnack.IsLocallyPerimeterMinimizing line 497
  28. def OAI.RPISingularHarnack.IsCone line 505