OAI/Probability/SwitchChain/SliceEuclideanGenerator.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Problem315.SliceEuclideanGenerator.State line 11
  2. def OAI.Problem315.SliceEuclideanGenerator.relabel line 14
  3. theorem OAI.Problem315.SliceEuclideanGenerator.relabel_val line 24
  4. def OAI.Problem315.SliceEuclideanGenerator.swapState line 27
  5. theorem OAI.Problem315.SliceEuclideanGenerator.swapState_twice line 30
  6. def OAI.Problem315.SliceEuclideanGenerator.moveOperator line 35
  7. theorem OAI.Problem315.SliceEuclideanGenerator.moveOperator_apply line 41
  8. theorem OAI.Problem315.SliceEuclideanGenerator.moveOperator_twice line 45
  9. theorem OAI.Problem315.SliceEuclideanGenerator.moveOperator_symmetric line 51
  10. theorem OAI.Problem315.SliceEuclideanGenerator.move_energy line 59
  11. def OAI.Problem315.SliceEuclideanGenerator.generator line 71
  12. theorem OAI.Problem315.SliceEuclideanGenerator.generator_apply line 75
  13. theorem OAI.Problem315.SliceEuclideanGenerator.generator_symmetric line 83
  14. theorem OAI.Problem315.SliceEuclideanGenerator.generator_energy line 91
  15. theorem OAI.Problem315.SliceEuclideanGenerator.generator_positive line 99