OAI/Geometry/CubicTorus/Reflection/ChamberGlobalFold.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.abs_shortestLift_coordinate line 13
  2. def OAI.CubicTorus.chamberFoldLift line 19
  3. lemma OAI.CubicTorus.chamberFoldLift_apply line 23
  4. lemma OAI.CubicTorus.chamberFoldLift_mem line 27
  5. lemma OAI.CubicTorus.chamberFoldLift_mem_iff line 33
  6. def OAI.CubicTorus.chamberVertex line 38
  7. lemma OAI.CubicTorus.chamberVertex_mem line 41
  8. lemma OAI.CubicTorus.chamberVertex_sine_zero line 47
  9. lemma OAI.CubicTorus.chamberVertex_mono line 53
  10. lemma OAI.CubicTorus.chamberVertex_bottom line 60
  11. lemma OAI.CubicTorus.chamberVertex_bottom_le line 63
  12. lemma OAI.CubicTorus.chamberVertex_le_top line 68
  13. lemma OAI.CubicTorus.isMinimizerAt_openRepresentative_nonempty line 84
  14. lemma OAI.CubicTorus.isMinimizerAt_vacant_nonempty line 93
  15. lemma OAI.CubicTorus.mem_open_of_mem_closure_not_frontier line 103
  16. theorem OAI.CubicTorus.isMinimizerAt_chamber_vertex_order line 110
  17. theorem OAI.CubicTorus.isMinimizerAt_vacant_face line 140
  18. theorem OAI.CubicTorus.isMinimizerAt_exists_positive_sides line 176
  19. lemma OAI.CubicTorus.isCompact_closedHalfBox line 202
  20. theorem OAI.CubicTorus.isMinimizerAt_chamber_face_gap line 211
  21. theorem OAI.CubicTorus.isMinimizerAt_tangent_graph_cover line 252
  22. theorem OAI.CubicTorus.isMinimizerAt_normal_line_isolated line 275
  23. lemma OAI.CubicTorus.hasDerivAt_zero_isolated line 305
  24. theorem OAI.CubicTorus.isMinimizerAt_transverse_line_isolated line 321
  25. lemma OAI.CubicTorus.coordinateHalf_pair line 370
  26. lemma OAI.CubicTorus.isMinimizerAt_normal_nonzero_off_seam line 392
  27. lemma OAI.CubicTorus.countable_axial_sine_zeros line 420
  28. theorem OAI.CubicTorus.isMinimizerAt_countable_axial_boundary line 430
  29. lemma OAI.CubicTorus.mem_coordinateHalf_of_chamber_interval line 483
  30. lemma OAI.CubicTorus.chamber_zero_normal_endpoint line 500
  31. def OAI.CubicTorus.chamberAxialCritical line 514
  32. lemma OAI.CubicTorus.isCompact_chamberAxialCritical line 518
  33. theorem OAI.CubicTorus.isMinimizerAt_finite_chamber_critical line 530
  34. theorem OAI.CubicTorus.isMinimizerAt_finite_exceptional_heights line 597
  35. theorem OAI.CubicTorus.monotone_path_unique_exit line 620
  36. def OAI.CubicTorus.chamberSegment line 725
  37. lemma OAI.CubicTorus.chamberSegment_apply line 727
  38. lemma OAI.CubicTorus.chamberSegment_mem line 730
  39. lemma OAI.CubicTorus.chamberSegment_mono line 739
  40. theorem OAI.CubicTorus.chamberSegment_normal_positive line 745
  41. theorem OAI.CubicTorus.isMinimizerAt_chamber_unique_ray_exit line 781