OAI/Geometry/CubicTorus/Reflection/CoordinateChamber.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.congruentAE_of_translated line 13
  2. theorem OAI.CubicTorus.isMinimizerAt_standard_or_strict_reflection line 35
  3. lemma OAI.CubicTorus.normalMeasure_test_translation_nonneg line 74
  4. theorem OAI.CubicTorus.isMinimizerAt_monotone_translation_test line 119
  5. lemma OAI.CubicTorus.exists_open_swept_neighborhood line 151
  6. theorem OAI.CubicTorus.isMinimizerAt_no_reverse_crossing line 167
  7. lemma OAI.CubicTorus.isMinimizerAt_regular_openRepresentative line 245
  8. theorem OAI.CubicTorus.isMinimizerAt_monotone_segment line 259
  9. theorem OAI.CubicTorus.isMinimizerAt_monotone_segment_closure line 279
  10. def OAI.CubicTorus.coordinateChamber line 307
  11. def OAI.CubicTorus.chamberCorner line 310
  12. lemma OAI.CubicTorus.coordinateChamber_open line 313
  13. lemma OAI.CubicTorus.mem_chamber_of_coordinates line 322
  14. lemma OAI.CubicTorus.isMinimizerAt_normal_positive_opposite_half line 342
  15. theorem OAI.CubicTorus.isMinimizerAt_exists_positive_chamber line 370
  16. theorem OAI.CubicTorus.isMinimizerAt_chamber_downset line 395
  17. def OAI.CubicTorus.openHalfBox line 438
  18. def OAI.CubicTorus.closedHalfBox line 439
  19. lemma OAI.CubicTorus.closure_openHalfBox line 441
  20. lemma OAI.CubicTorus.isOpen_openHalfBox line 456
  21. lemma OAI.CubicTorus.halfBox_downset_closure line 463
  22. theorem OAI.CubicTorus.isMinimizerAt_chamber_closed_downset_of_open line 498
  23. def OAI.CubicTorus.foldCoordinate line 529
  24. lemma OAI.CubicTorus.foldCoordinate_apply line 532
  25. lemma OAI.CubicTorus.foldCoordinate_continuous line 539
  26. lemma OAI.CubicTorus.quotientMap_centered_reflection line 544
  27. lemma OAI.CubicTorus.foldCoordinate_quotient_alternative line 558
  28. def OAI.CubicTorus.localFoldCoordinate line 576
  29. def OAI.CubicTorus.localChamberFold line 580
  30. lemma OAI.CubicTorus.localFoldCoordinate_apply line 583
  31. lemma OAI.CubicTorus.localChamberFold_apply line 591
  32. lemma OAI.CubicTorus.localFoldCoordinate_continuous line 597
  33. lemma OAI.CubicTorus.localChamberFold_continuous line 602
  34. lemma OAI.CubicTorus.localChamberFold_fixed line 606
  35. lemma OAI.CubicTorus.localChamberFold_mem_eventually line 614
  36. lemma OAI.CubicTorus.localFoldCoordinate_preserves line 643
  37. lemma OAI.CubicTorus.localChamberFold_preserves line 666
  38. lemma OAI.CubicTorus.quotientMap_isOpenMap line 685
  39. lemma OAI.CubicTorus.openRepresentative_reflection_invariant line 694
  40. lemma OAI.CubicTorus.chamber_closure_from_interior line 699
  41. theorem OAI.CubicTorus.isMinimizerAt_chamber_closed_downset line 721
  42. lemma OAI.CubicTorus.localChamberFold_mem_iff line 751
  43. lemma OAI.CubicTorus.reflection_invariant_closure line 763
  44. lemma OAI.CubicTorus.chamber_open_downset_of_closed line 773
  45. theorem OAI.CubicTorus.isMinimizerAt_chamber_open_downset line 807