OAI/Geometry/CubicTorus/Reflection/MinimizerAxialCenter.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicTorus.isMinimizerAt_normal_one_sign_zero line 13
  2. theorem OAI.CubicTorus.isMinimizerAt_normal_coordinate_strict_or_zero line 92
  3. lemma OAI.CubicTorus.isMinimizerAt_normal_unit_boundary line 142
  4. theorem OAI.CubicTorus.isMinimizerAt_reflection_vertex_excluded line 154
  5. theorem OAI.CubicTorus.isMinimizerAt_connected_reflection_geometry line 172
  6. lemma OAI.CubicTorus.normalGraph_tangent_line line 218
  7. theorem OAI.CubicTorus.isMinimizerAt_zero_normal_local_flow line 259
  8. lemma OAI.CubicTorus.graph_tangent_fderiv_zero line 294
  9. theorem OAI.CubicTorus.isMinimizerAt_tangent_fderiv_zero line 314
  10. theorem OAI.CubicTorus.isMinimizerAt_axial_shape_zero line 338
  11. lemma OAI.CubicTorus.plane_symmetric_null_shape line 375
  12. lemma OAI.CubicTorus.normal_plane_trace line 415
  13. lemma OAI.CubicTorus.normal_axial_shape line 429
  14. def OAI.CubicTorus.axialCenter line 470
  15. lemma OAI.CubicTorus.axialCenter_fderiv line 473
  16. theorem OAI.CubicTorus.isMinimizerAt_axial_shape line 482
  17. theorem OAI.CubicTorus.isMinimizerAt_axialCenter_local line 506
  18. def OAI.CubicTorus.axialProjection line 571
  19. lemma OAI.CubicTorus.axialProjection_apply line 574
  20. lemma OAI.CubicTorus.axialProjection_self line 577
  21. lemma OAI.CubicTorus.axialProjection_tangent line 580
  22. lemma OAI.CubicTorus.axialProjection_inner line 582
  23. lemma OAI.CubicTorus.axialProjection_inner_zero line 587
  24. lemma OAI.CubicTorus.axialProjection_idempotent line 591
  25. def OAI.CubicTorus.euclideanCylinder line 595
  26. lemma OAI.CubicTorus.isClosed_euclideanCylinder line 598
  27. lemma OAI.CubicTorus.normal_squared_cylinder_difference line 601
  28. lemma OAI.CubicTorus.local_graph_cylinder_iff line 623
  29. lemma OAI.CubicTorus.axialCenter_transverse line 662
  30. lemma OAI.CubicTorus.cylinder_center_translation line 667
  31. theorem OAI.CubicTorus.isMinimizerAt_axial_local_cylinder line 679
  32. lemma OAI.CubicTorus.isPreconnected_euclideanCylinder line 745
  33. theorem OAI.CubicTorus.closed_cylindrical_set_contains_cylinder line 776
  34. lemma OAI.CubicTorus.coordinateAxis_norm line 820
  35. lemma OAI.CubicTorus.axialProjection_axis_apply line 822
  36. lemma OAI.CubicTorus.axialProjection_axis_lattice line 830
  37. lemma OAI.CubicTorus.axialCenter_axis_periodic line 838
  38. lemma OAI.CubicTorus.fin_three_other_coordinates line 851