OAI/Probability/BinarySweep/Analytic/OneAxis.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.BinaryCoordinateSweeps.oneAxisOutsideEmpty line 14
  2. def OAI.BinaryCoordinateSweeps.oneAxisSlotEquiv line 17
  3. def OAI.BinaryCoordinateSweeps.oneAxisChoiceEquiv line 19
  4. def OAI.BinaryCoordinateSweeps.oneAxisSweepEquiv line 22
  5. lemma OAI.BinaryCoordinateSweeps.oneAxisSweepEquiv_apply line 26
  6. lemma OAI.BinaryCoordinateSweeps.oneAxis_pathEvent_iff line 51
  7. def OAI.BinaryCoordinateSweeps.assignmentResidualEquiv line 61
  8. lemma OAI.BinaryCoordinateSweeps.assignmentResidualEquiv_apply line 82
  9. def OAI.BinaryCoordinateSweeps.oneAxisRemainingEquiv line 89
  10. lemma OAI.BinaryCoordinateSweeps.oneAxisRemainingEquiv_apply line 98
  11. lemma OAI.BinaryCoordinateSweeps.oneAxis_gridWeight line 116
  12. lemma OAI.BinaryCoordinateSweeps.oneAxis_gridWeight_zero line 120
  13. lemma OAI.BinaryCoordinateSweeps.oneAxis_conditionalOperator_zero line 127