OAI/Probability/BinarySweep/Trajectories/Trajectory.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BinaryCoordinateSweeps.trajectory_coordinates line 12
  2. lemma OAI.BinaryCoordinateSweeps.trajectory_unique line 39
  3. def OAI.BinaryCoordinateSweeps.gridPartialSweep line 47
  4. lemma OAI.BinaryCoordinateSweeps.gridPartialSweep_zero line 51
  5. lemma OAI.BinaryCoordinateSweeps.gridPartialSweep_last line 54
  6. lemma OAI.BinaryCoordinateSweeps.gridPartialSweep_succ line 59
  7. lemma OAI.BinaryCoordinateSweeps.gridLayer_other line 67
  8. lemma OAI.BinaryCoordinateSweeps.gridPartialSweep_changes line 71
  9. lemma OAI.BinaryCoordinateSweeps.gridPartialSweep_path line 76
  10. lemma OAI.BinaryCoordinateSweeps.pathEvent_of_endpoints line 84
  11. def OAI.BinaryCoordinateSweeps.augmentByChoice line 101
  12. def OAI.BinaryCoordinateSweeps.augmentByChoice_extension line 108
  13. lemma OAI.BinaryCoordinateSweeps.placementEvent_iff_augmentation line 116
  14. lemma OAI.BinaryCoordinateSweeps.placementProbability_augmentation line 142
  15. theorem OAI.BinaryCoordinateSweeps.placement_probability_cost line 151
  16. lemma OAI.BinaryCoordinateSweeps.placementProbability_pos_has_choice line 161
  17. def OAI.BinaryCoordinateSweeps.realizePlacement line 177
  18. lemma OAI.BinaryCoordinateSweeps.realizePlacement_spec line 183
  19. def OAI.BinaryCoordinateSweeps.placementTransitionCost line 190
  20. theorem OAI.BinaryCoordinateSweeps.placement_probability_cost_of_pos line 196