OAI/Geometry/CubicTorus/Estimates/TorusCoordinatePermute.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicTorus.circle_equality_phase_interval line 14
  2. lemma OAI.CubicTorus.circle_coe_integer_zero line 84
  3. lemma OAI.CubicTorus.circle_image_interval_eq_ball line 88
  4. lemma OAI.CubicTorus.circle_interval_ae_ball line 111
  5. theorem OAI.CubicTorus.circle_equality_phase_ball line 149
  6. def OAI.CubicTorus.torusCoordinatePermute line 180
  7. lemma OAI.CubicTorus.coordinate_ball_isometric_slab line 190
  8. lemma OAI.CubicTorus.integerCharacter_single line 216
  9. theorem OAI.CubicTorus.unit_character_equality_congruent_slab line 221
  10. theorem OAI.CubicTorus.Periodic.isMinimizerAt_connected_or_coordinate_slab line 264
  11. lemma OAI.CubicTorus.openRepresentative_congr_ae line 319
  12. lemma OAI.CubicTorus.isMinimizerAt_frontier_compl line 327
  13. theorem OAI.CubicTorus.Periodic.isMinimizerAt_connected_or_standard_slab line 347
  14. theorem OAI.CubicTorus.isMinimizerAt_integral_curvature_zero_slab line 377
  15. theorem OAI.CubicTorus.isMinimizerAt_connected_curvature_integral_pos line 437
  16. theorem OAI.CubicTorus.Periodic.isMinimizerAt_connected_strict_support line 461
  17. theorem OAI.CubicTorus.Periodic.isMinimizerAt_profile_local_min_slab line 481
  18. lemma OAI.CubicTorus.Reduction.second_deriv_nonneg_of_right_min line 515
  19. theorem OAI.CubicTorus.Periodic.isMinimizerAt_connected_positive_CMC line 540
  20. lemma OAI.CubicTorus.Reduction.second_deriv_nonneg_of_left_min line 579
  21. theorem OAI.CubicTorus.Periodic.connected_support_of_CMC line 604
  22. theorem OAI.CubicTorus.Periodic.connected_CMC_strict_sign line 622
  23. theorem OAI.CubicTorus.Periodic.isMinimizerAt_zero_CMC_slab line 660
  24. lemma OAI.CubicTorus.planeTraceSquare_symmetric_equality line 688
  25. theorem OAI.CubicTorus.graph_curvature_equality_umbilic line 708
  26. theorem OAI.CubicTorus.graph_umbilic_CMC_center line 755
  27. theorem OAI.CubicTorus.graph_umbilic_CMC_sphere line 790
  28. lemma OAI.CubicTorus.normal_squared_distance_difference line 817