OAI/Geometry/CubicTorus/Regularity/BVLipschitzGraph.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.trapped_characteristic line 15
  2. theorem OAI.CubicTorus.normalMeasure_trapped_projection line 48
  3. lemma OAI.CubicTorus.unit_normal_sq_distance line 82
  4. theorem OAI.CubicTorus.normalMeasure_trapped_excess line 87
  5. lemma OAI.CubicTorus.gradient_of_notMem_tsupport line 134
  6. lemma OAI.CubicTorus.gradient_tsupport_subset line 138
  7. theorem OAI.CubicTorus.normalMeasure_local_laplacian line 145
  8. theorem OAI.CubicTorus.weakCMC_scalar_residual_identity line 157
  9. theorem OAI.CubicTorus.weakCMC_scalar_residual_bound line 203
  10. lemma OAI.CubicTorus.normalMeasure_frontier_ae line 241
  11. lemma OAI.CubicTorus.trapped_frontier_height line 254
  12. theorem OAI.CubicTorus.normalMeasure_trapped_test_derivative_zero line 278
  13. theorem OAI.CubicTorus.weakCMC_trapped_scalar_identity line 292
  14. lemma OAI.CubicTorus.good_scales_boundary_cone line 327
  15. def OAI.CubicTorus.normalPlaneProjection line 386
  16. lemma OAI.CubicTorus.normalPlaneProjection_sub line 388
  17. lemma OAI.CubicTorus.normalPlaneProjection_inner line 393
  18. lemma OAI.CubicTorus.norm_le_two_normalPlaneProjection line 398
  19. lemma OAI.CubicTorus.exists_lipschitz_height_of_cone line 406
  20. lemma OAI.CubicTorus.lifted_cone_of_torus_cone line 453
  21. lemma OAI.CubicTorus.ediam_metricBall_le line 479
  22. lemma OAI.CubicTorus.hausdorff_two_le_of_lower_density line 486
  23. theorem OAI.CubicTorus.isMinimizerAt_finite_boundary_area line 551
  24. lemma OAI.CubicTorus.hausdorff_two_le_open_of_lower_density line 575
  25. lemma OAI.CubicTorus.hausdorff_two_le_measure_of_lower_density line 664
  26. lemma OAI.CubicTorus.hausdorff_two_null_of_lower_density line 680
  27. theorem OAI.CubicTorus.isMinimizerAt_boundary_area_absolutelyContinuous line 691
  28. lemma OAI.CubicTorus.singleton_null_of_quadratic_upper_density line 717
  29. lemma OAI.CubicTorus.measure_le_hausdorff_two_of_upper_density line 733
  30. theorem OAI.CubicTorus.isMinimizerAt_perimeter_absolutelyContinuous_area line 779
  31. lemma OAI.CubicTorus.measure_bad_scales_le line 817