OAI/Geometry/CubicTorus/Rigidity/LocalGraphSphere.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.local_graph_sphere_iff line 13
  2. theorem OAI.CubicTorus.closed_spherical_set_contains_sphere line 50
  3. lemma OAI.CubicTorus.norm_quotientMap_eq_of_half_cube line 102
  4. lemma OAI.CubicTorus.shortestLift_half_cube line 112
  5. theorem OAI.CubicTorus.smallBall_exterior_preconnected line 117
  6. theorem OAI.CubicTorus.isMinimizerAt_umbilic_local_sphere line 193
  7. theorem OAI.CubicTorus.periodic_local_constant_on_preconnected line 291
  8. theorem OAI.CubicTorus.periodic_complete_sphere_radius_lt_half line 335
  9. theorem OAI.CubicTorus.periodic_connected_spherical_boundary line 389
  10. theorem OAI.CubicTorus.isMinimizerAt_mean_square_equality_spherical line 444
  11. lemma OAI.CubicTorus.Reduction.second_deriv_sub_affine line 539
  12. theorem OAI.CubicTorus.Reduction.UpperSupport.power_affine_jet_nonneg line 549
  13. theorem OAI.CubicTorus.Periodic.isMinimizerAt_power_affine_spherical line 583
  14. lemma OAI.CubicTorus.quotientMap_image_small_sphere line 635
  15. lemma OAI.CubicTorus.torus_ball_preconnected line 651
  16. lemma OAI.CubicTorus.torus_smallBall_exterior_preconnected line 655
  17. lemma OAI.CubicTorus.preconnected_avoiding_frontier line 668
  18. theorem OAI.CubicTorus.isMinimizerAt_spherical_boundary_phase line 683
  19. theorem OAI.CubicTorus.Periodic.isMinimizerAt_power_affine_ball_or_complement line 746
  20. lemma OAI.CubicTorus.metricBall_eq_translate line 768
  21. lemma OAI.CubicTorus.metricBall_volume line 773
  22. lemma OAI.CubicTorus.metricBall_perimeter line 778
  23. lemma OAI.CubicTorus.small_minimizer_ball_phase line 785
  24. theorem OAI.CubicTorus.isMinimizerAt_spherical_standard_ball line 812