OAI/Probability/ThorpShuffle/HalfHistories.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Thorp.Conditional.RawState line 16
  2. def OAI.Thorp.Conditional.rawNext line 20
  3. def OAI.Thorp.Conditional.rawIterate line 24
  4. def OAI.Thorp.Conditional.CenteredState.raw line 29
  5. theorem OAI.Thorp.Conditional.iterateState_raw line 31
  6. theorem OAI.Thorp.Conditional.rawIterate_free line 41
  7. theorem OAI.Thorp.Conditional.mean_bool line 52
  8. theorem OAI.Thorp.Conditional.pairUpdate_mean_fst line 55
  9. theorem OAI.Thorp.Conditional.pairUpdate_mean_snd line 59
  10. theorem OAI.Thorp.Conditional.mean_sign line 64
  11. theorem OAI.Thorp.Conditional.mean_coin_eval line 68
  12. theorem OAI.Thorp.Conditional.mean_physicalFlow_snoc line 80
  13. def OAI.Thorp.Conditional.firstMean line 104
  14. def OAI.Thorp.Conditional.meanLayer line 107
  15. theorem OAI.Thorp.Conditional.mean_physicalFlow line 111
  16. theorem OAI.Thorp.Conditional.init_cons line 120
  17. theorem OAI.Thorp.Conditional.meanLayer_lift line 126
  18. theorem OAI.Thorp.Conditional.mean_iterations_dimension line 138
  19. theorem OAI.Thorp.Conditional.mean_firstMean line 147
  20. theorem OAI.Thorp.Conditional.mean_iterations_sweep line 154
  21. theorem OAI.Thorp.Conditional.mean_rawIterate_weight line 164
  22. theorem OAI.Thorp.Conditional.mean_rawIterate_sweep line 186
  23. theorem OAI.Thorp.Conditional.rawIterate_indicator line 192
  24. theorem OAI.Thorp.Conditional.mean_free_after_sweep line 204