OAI/Geometry/CubicTorus/Estimates/BVGraphEnergy.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.graph_derivative_norm_le_tilt line 15
  2. lemma OAI.CubicTorus.normalGraph_gradient_bound_ae line 43
  3. lemma OAI.CubicTorus.normalGraph_antilipschitz line 65
  4. lemma OAI.CubicTorus.normalGraph_torus_antilipschitz line 86
  5. instance OAI.CubicTorus.plane_hausdorff_two_haar line 101
  6. lemma OAI.CubicTorus.normalGraph_preimage_area_null line 106
  7. lemma OAI.CubicTorus.isMinimizerAt_ae_on_normalGraph line 125
  8. theorem OAI.CubicTorus.isMinimizerAt_normalGraph_gradient_bound line 143
  9. def OAI.CubicTorus.planeAreaFactor line 177
  10. lemma OAI.CubicTorus.normalGraph_preimage_volume_le line 180
  11. lemma OAI.CubicTorus.normalGraph_map_volume_le_perimeter line 202
  12. theorem OAI.CubicTorus.isMinimizerAt_normalGraph_good_energy line 239
  13. def OAI.CubicTorus.normalPlaneCoordinates line 300
  14. lemma OAI.CubicTorus.normalPlaneCoordinates_embedding line 303
  15. lemma OAI.CubicTorus.normalPlaneCoordinates_normal line 310
  16. lemma OAI.CubicTorus.normalPlaneCoordinates_lipschitz line 317
  17. lemma OAI.CubicTorus.normalPlaneCoordinates_graph line 323
  18. lemma OAI.CubicTorus.normalPlaneCoordinates_torus_lipschitz line 328
  19. lemma OAI.CubicTorus.exists_frontier_on_interval line 341
  20. lemma OAI.CubicTorus.trapped_boundary_projects_disk line 360
  21. lemma OAI.CubicTorus.plane_projection_volume_le_perimeter line 410
  22. lemma OAI.CubicTorus.normalPlaneCoordinates_reconstruct line 434
  23. lemma OAI.CubicTorus.trapped_graph_holes_volume_le line 446
  24. theorem OAI.CubicTorus.isMinimizerAt_normalGraph_full_energy line 495
  25. theorem OAI.CubicTorus.normalMeasure_lipschitz_approximation_with_cone line 597
  26. theorem OAI.CubicTorus.isMinimizerAt_lipschitz_approximation_with_cone line 664
  27. lemma OAI.CubicTorus.normalPlaneEmbedding_coordinates line 719
  28. lemma OAI.CubicTorus.good_cone_column_unique line 725
  29. lemma OAI.CubicTorus.phases_of_unique_frontier line 749
  30. theorem OAI.CubicTorus.trapped_good_column_phases line 776