OAI/Geometry/CubicTorus/Reflection/SiblingAxialProjection.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicTorus.Periodic.isMinimizerAt_selected_nodal_irreducible line 14
  2. lemma OAI.CubicTorus.positiveNodalPiece_relative_compl line 87
  3. lemma OAI.CubicTorus.positiveBoundaryDomain_preconnected line 103
  4. lemma OAI.CubicTorus.positiveNodalPiece_eq_positive_locus line 108
  5. theorem OAI.CubicTorus.Periodic.isMinimizerAt_translation_signs_preconnected line 134
  6. theorem OAI.CubicTorus.Periodic.isMinimizerAt_slab_or_translation_signs line 184
  7. lemma OAI.CubicTorus.odd_preconnected_sign_half line 224
  8. theorem OAI.CubicTorus.isMinimizerAt_any_normal_signs line 259
  9. theorem OAI.CubicTorus.isMinimizerAt_reflection_weak_normal_sign line 294
  10. theorem OAI.CubicTorus.isMinimizerAt_normal_strong_minimum line 330
  11. theorem OAI.CubicTorus.isMinimizerAt_reflection_strict_normal_sign line 362
  12. theorem OAI.CubicTorus.normal_zero_translation_ae line 417
  13. theorem OAI.CubicTorus.isMinimizerAt_zero_normal_invariant line 454
  14. lemma OAI.CubicTorus.normalizedCMCCharts_zero_component_differential line 491
  15. theorem OAI.CubicTorus.isMinimizerAt_zero_component_shape_kernel line 520
  16. theorem OAI.CubicTorus.isMinimizerAt_zero_component_shape line 553
  17. theorem OAI.CubicTorus.isMinimizerAt_zero_component_curvature line 576
  18. def OAI.CubicTorus.sibling_axialProjection line 610
  19. lemma OAI.CubicTorus.sibling_axialProjection_apply line 613
  20. lemma OAI.CubicTorus.axialProjection_fixed line 615
  21. lemma OAI.CubicTorus.graphSlopeNormal_inner_fderiv line 618
  22. theorem OAI.CubicTorus.normalizedCMCCharts_axial_local_center line 631
  23. theorem OAI.CubicTorus.isMinimizerAt_zero_component_local_center line 684
  24. def OAI.CubicTorus.axialCylinder line 714
  25. lemma OAI.CubicTorus.sibling_axialProjection_inner line 717
  26. lemma OAI.CubicTorus.axial_normal_squared_distance_difference line 721
  27. lemma OAI.CubicTorus.sibling_local_graph_cylinder_iff line 742
  28. theorem OAI.CubicTorus.isMinimizerAt_zero_component_local_cylinder line 768