OAI/Probability/ThorpShuffle/PairAveraging.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Thorp.Conditional.mean line 16
  2. def OAI.Thorp.Conditional.sign line 19
  3. theorem OAI.Thorp.Conditional.sign_not line 21
  4. theorem OAI.Thorp.Conditional.sign_sq line 24
  5. theorem OAI.Thorp.Conditional.sign_mul_self line 27
  6. def OAI.Thorp.Conditional.toggleCoin line 30
  7. theorem OAI.Thorp.Conditional.toggleCoin_apply line 39
  8. theorem OAI.Thorp.Conditional.sum_sign line 43
  9. theorem OAI.Thorp.Conditional.sum_sign_pair line 49
  10. theorem OAI.Thorp.Conditional.mean_signed_sum_sq line 62
  11. def OAI.Thorp.Conditional.pairUpdate line 93
  12. theorem OAI.Thorp.Conditional.pairUpdate_sum line 97
  13. theorem OAI.Thorp.Conditional.pairUpdate_difference line 101
  14. theorem OAI.Thorp.Conditional.pairUpdate_mean_first line 106
  15. theorem OAI.Thorp.Conditional.pairUpdate_difference_sq line 110
  16. def OAI.Thorp.Conditional.flow line 116
  17. def OAI.Thorp.Conditional.oddCoefficient line 122
  18. theorem OAI.Thorp.Conditional.mean_oddCoefficient_sq line 125
  19. def OAI.Thorp.Conditional.pairMap line 152
  20. theorem OAI.Thorp.Conditional.pairMap_involutive line 155
  21. theorem OAI.Thorp.Conditional.flow_sub line 160
  22. theorem OAI.Thorp.Conditional.flow_uniform line 167
  23. theorem OAI.Thorp.Conditional.flow_support line 175
  24. theorem OAI.Thorp.Conditional.flow_evenCoefficient line 184
  25. theorem OAI.Thorp.Conditional.flow_sum line 192
  26. theorem OAI.Thorp.Conditional.pairUpdate_energy_le line 201
  27. theorem OAI.Thorp.Conditional.flow_energy_le line 207
  28. theorem OAI.Thorp.Conditional.pairUpdate_first_noise line 216
  29. theorem OAI.Thorp.Conditional.pairUpdate_second_noise line 221