OAI/Geometry/CubicTorus/Profiles/FlatTranslation.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicTorus.isMinimizerAt_positive_support_spherical line 15
  2. theorem OAI.CubicTorus.isMinimizerAt_strict_one_vertex_spherical line 100
  3. theorem OAI.CubicTorus.isMinimizerAt_nonstandard_occupied_axial_vertex line 146
  4. lemma OAI.CubicTorus.CongruentAE.isometry_preimage line 193
  5. lemma OAI.CubicTorus.smallStandardRegion_isometry_preimage line 209
  6. lemma OAI.CubicTorus.standardRegionAt_isometry_preimage line 217
  7. lemma OAI.CubicTorus.standardRegionAt_isometry_preimage_iff line 225
  8. def OAI.CubicTorus.flatTranslation line 236
  9. theorem OAI.CubicTorus.isMinimizerAt_nonstandard_small_side_vertices line 254
  10. lemma OAI.CubicTorus.three_axes_dichotomy line 292
  11. theorem OAI.CubicTorus.isMinimizerAt_nonstandard_V2_axial_patterns line 312
  12. lemma OAI.CubicTorus.axisReflection_eq_coordinateReflection line 346
  13. lemma OAI.CubicTorus.quotient_orientedUpperVertex_eq line 354
  14. theorem OAI.CubicTorus.isMinimizerAt_chamber_upper_downset line 364
  15. lemma OAI.CubicTorus.positiveNodalPiece_separator_positive line 425
  16. lemma OAI.CubicTorus.positiveNodalPiece_separator_negative line 445
  17. theorem OAI.CubicTorus.double_reflection_nodal_vanish line 452
  18. theorem OAI.CubicTorus.exists_odd_periodic_local_identity line 509
  19. theorem OAI.CubicTorus.TrueRadialTube.odd_periodic_transverse_germs line 534
  20. theorem OAI.CubicTorus.TrueRadialTube.exists_odd_rotation_nodal_restriction line 557
  21. lemma OAI.CubicTorus.odd_periodic_chamberCorner line 616
  22. lemma OAI.CubicTorus.periodicRotationNormalScalar_apply line 627
  23. lemma OAI.CubicTorus.isMinimizerAt_normal_reflection_apply line 638
  24. lemma OAI.CubicTorus.isMinimizerAt_rotation_reflection_odd line 652
  25. lemma OAI.CubicTorus.descent_coordinateSine_other_reflection line 689
  26. theorem OAI.CubicTorus.TrueRadialTube.exists_rotation_zero line 697
  27. lemma OAI.CubicTorus.coordinatePlaneLift_quarter_inner line 757
  28. lemma OAI.CubicTorus.coordinatePlaneLift_frame_norm line 764
  29. lemma OAI.CubicTorus.coordinateSectionPoint_axial_hasDerivAt line 775
  30. theorem OAI.CubicTorus.TrueRadialTube.radial_independent_angle line 783