OAI/Probability/ThorpShuffle/NoiseEnergy.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Thorp.Conditional.insertBit line 14
  2. def OAI.Thorp.Conditional.halfPositionEquiv line 17
  3. theorem OAI.Thorp.Conditional.halfPositionEquiv_apply line 20
  4. theorem OAI.Thorp.Conditional.insertBit_zero line 23
  5. theorem OAI.Thorp.Conditional.insertBit_last line 26
  6. theorem OAI.Thorp.Conditional.insertBit_cons line 29
  7. theorem OAI.Thorp.Conditional.insertBit_snoc line 39
  8. theorem OAI.Thorp.Conditional.physicalFree_snoc line 50
  9. theorem OAI.Thorp.Conditional.physicalFlow_snoc line 56
  10. theorem OAI.Thorp.Conditional.RawState.ext line 66
  11. def OAI.Thorp.Conditional.halfRaw line 70
  12. theorem OAI.Thorp.Conditional.rawNext_half line 74
  13. def OAI.Thorp.Conditional.halfMarker line 99
  14. def OAI.Thorp.Conditional.coinHalfMarker line 100
  15. theorem OAI.Thorp.Conditional.halfMarker_zero line 102
  16. theorem OAI.Thorp.Conditional.halfMarker_end line 103
  17. theorem OAI.Thorp.Conditional.halfMarker_next line 106
  18. theorem OAI.Thorp.Conditional.halfMarker_previous line 110
  19. def OAI.Thorp.Conditional.halfHistory line 114
  20. theorem OAI.Thorp.Conditional.halfHistory_snoc line 117
  21. theorem OAI.Thorp.Conditional.rawIterate_half line 133
  22. def OAI.Thorp.Conditional.splitHalfHistory line 146
  23. theorem OAI.Thorp.Conditional.mean_half_product line 163
  24. theorem OAI.Thorp.Conditional.mean_opposite_half_product line 173