OAI/Geometry/Perimeter/Regularity/ExistsDiameterCoverOfHausdorffZero.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RPI.exists_diameter_cover_of_hausdorff_zero line 15
2. theorem OAI.RPI.exists_finite_ball_cover_of_hausdorff_zero line 38
3. theorem OAI.RPI.innerCapacityBump_energy_le_radius_power line 150
4. theorem OAI.RPI.exists_smooth_capacity_cutoff line 169
5. theorem OAI.RPI.exists_smooth_capacity_sequence line 238
6. theorem OAI.RPI.projected_smooth_energy_le line 279
7. theorem OAI.RPI.projected_smooth_energy_tendsto_zero line 296
8. theorem OAI.RPI.hausdorff_capacity_dimension line 305
9. theorem OAI.RPI.Boundary.exists_memLp_capacity_sequence line 324
10. theorem OAI.RPI.Boundary.hausdorff_trace_mem_sobolevGraph line 367
11. theorem OAI.RPI.Boundary.tangentPlane_eq_ker_of_local_level line 399
12. theorem OAI.RPI.Boundary.surfaceGradient_eq_level_formula line 461
13. theorem OAI.RPI.Boundary.continuousAt_gradient_of_contDiffAt line 487