OAI/Geometry/CubicTorus/Regularity/GraphNormalExtensionDivergence.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicTorus.graph_normal_extension_divergence line 13
  2. theorem OAI.CubicTorus.actual_centered_normal_geometry line 89
  3. theorem OAI.CubicTorus.isMinimizerAt_normal_geometry line 116
  4. theorem OAI.CubicTorus.isMinimizerAt_normal_curvature_nonnegative line 173
  5. theorem OAI.CubicTorus.Periodic.isMinimizerAt_curvature_stability line 195
  6. lemma OAI.CubicTorus.localRadialSquared_lt_iff line 227
  7. theorem OAI.CubicTorus.exists_periodic_local_cutoff line 235
  8. theorem OAI.CubicTorus.exists_periodic_smooth_separator line 273
  9. lemma OAI.CubicTorus.integrable_normal_base line 322
  10. lemma OAI.CubicTorus.normal_curvature_continuous line 328
  11. theorem OAI.CubicTorus.separated_boundary_curvature_zero line 333
  12. lemma OAI.CubicTorus.closed_not_preconnected_split line 462
  13. theorem OAI.CubicTorus.Periodic.isMinimizerAt_connected_or_zero_curvature line 484
  14. theorem OAI.CubicTorus.isMinimizerAt_mean_curvature_bound line 522
  15. theorem OAI.CubicTorus.Periodic.isMinimizerAt_connected_or_minimal_flat line 547
  16. theorem OAI.CubicTorus.isMinimizerAt_zero_curvature_locally_plane line 595
  17. theorem OAI.CubicTorus.isMinimizerAt_zero_curvature_local_normal line 627
  18. theorem OAI.CubicTorus.closed_flat_set_contains_plane line 695
  19. theorem OAI.CubicTorus.Periodic.isMinimizerAt_connected_or_complete_planes line 733