OAI/Geometry/CubicTorus/Profiles/MinimizerFirstTransitionTube.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.firstTransition_mem_Ioo_half line 13
  2. theorem OAI.CubicTorus.isMinimizerAt_first_transition_corner_excluded line 18
  3. theorem OAI.CubicTorus.isMinimizerAt_first_transition_nonstandard_corner_restriction line 45
  4. theorem OAI.CubicTorus.isMinimizerAt_first_transition_permuted_corner_excluded line 83
  5. theorem OAI.CubicTorus.isMinimizerAt_first_transition_any_corner_excluded line 120
  6. theorem OAI.CubicTorus.isMinimizerAt_smaller_side_double_vertices_vacant line 164
  7. lemma OAI.CubicTorus.fin3_pair_complement line 212
  8. theorem OAI.CubicTorus.isMinimizerAt_first_transition_atMostOne_axis line 217
  9. lemma OAI.CubicTorus.bool_vertex_two_point_ideal line 254
  10. theorem OAI.CubicTorus.isMinimizerAt_first_transition_nonstandard_two_vertices line 291
  11. lemma OAI.CubicTorus.coordinateSectionPoint_continuous_pair line 336
  12. theorem OAI.CubicTorus.isMinimizerAt_tubular_sections line 341
  13. theorem OAI.CubicTorus.tubular_radius_uniform line 415
  14. lemma OAI.CubicTorus.quotientMap_coordinateSectionPoint_int line 450
  15. lemma OAI.CubicTorus.coordinateSectionPoint_fold_axis line 459
  16. lemma OAI.CubicTorus.continuous_radial_phase line 506
  17. theorem OAI.CubicTorus.isMinimizerAt_contDiff_tube_radius line 543
  18. lemma OAI.CubicTorus.tubular_radius_extension line 605
  19. theorem OAI.CubicTorus.isMinimizerAt_smooth_tube_radius line 677
  20. def OAI.CubicTorus.TrueRadialTube line 722
  21. theorem OAI.CubicTorus.isMinimizerAt_two_vertices_smooth_tube line 737
  22. theorem OAI.CubicTorus.isMinimizerAt_first_transition_nonstandard_smooth_tube line 796