OAI/Probability/BinarySweep/FiniteLaws/OneCard.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BinaryCoordinateSweeps.coordinateLayer_apply_at line 15
  2. lemma OAI.BinaryCoordinateSweeps.coordinateLayer_apply_other line 20
  3. def OAI.BinaryCoordinateSweeps.binaryPosition line 25
  4. def OAI.BinaryCoordinateSweeps.binaryPartialSweep line 28
  5. lemma OAI.BinaryCoordinateSweeps.binaryPartialSweep_zero line 31
  6. lemma OAI.BinaryCoordinateSweeps.binaryPartialSweep_last line 34
  7. lemma OAI.BinaryCoordinateSweeps.binaryPartialSweep_succ line 39
  8. lemma OAI.BinaryCoordinateSweeps.singleCoordinate_trajectory line 47
  9. lemma OAI.BinaryCoordinateSweeps.binarySweep_endpoint_iff line 74
  10. lemma OAI.BinaryCoordinateSweeps.uniform_coin_evaluation line 108
  11. lemma OAI.BinaryCoordinateSweeps.uniform_independent_event line 114
  12. lemma OAI.BinaryCoordinateSweeps.uniform_pi_coin_evaluation line 127
  13. lemma OAI.BinaryCoordinateSweeps.binary_one_card line 146
  14. lemma OAI.BinaryCoordinateSweeps.uniform_one_card line 174
  15. lemma OAI.BinaryCoordinateSweeps.line_one_card line 191
  16. lemma OAI.BinaryCoordinateSweeps.line_one_card_ite line 197