OAI/Probability/ThorpShuffle/ConditionalFlow.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Thorp.Conditional.splitPosition line 16
  2. def OAI.Thorp.Conditional.scatterPosition line 19
  3. def OAI.Thorp.Conditional.physicalFlow line 22
  4. def OAI.Thorp.Conditional.physicalFree line 27
  5. theorem OAI.Thorp.Conditional.step_symm_scatter line 31
  6. theorem OAI.Thorp.Conditional.physicalFlow_scatter line 36
  7. theorem OAI.Thorp.Conditional.physicalFree_scatter line 42
  8. theorem OAI.Thorp.Conditional.physicalFlow_sum line 48
  9. theorem OAI.Thorp.Conditional.physicalFlow_energy_le line 60
  10. theorem OAI.Thorp.Conditional.physicalFlow_support line 72
  11. theorem OAI.Thorp.Conditional.physicalFlow_uniform line 81
  12. def OAI.Thorp.Conditional.freeCount line 89
  13. def OAI.Thorp.Conditional.centeredPoint line 92
  14. theorem OAI.Thorp.Conditional.freeCount_pos line 96
  15. theorem OAI.Thorp.Conditional.sum_free_indicator line 101
  16. theorem OAI.Thorp.Conditional.centeredPoint_sum line 105
  17. theorem OAI.Thorp.Conditional.centeredPoint_support line 113
  18. theorem OAI.Thorp.Conditional.centeredPoint_energy line 119
  19. structure OAI.Thorp.Conditional.CenteredState line 137
  20. def OAI.Thorp.Conditional.initialState line 144
  21. def OAI.Thorp.Conditional.nextState line 154
  22. def OAI.Thorp.Conditional.iterateState line 162
  23. def OAI.Thorp.Conditional.expectedEnergy line 167
  24. theorem OAI.Thorp.Conditional.expectedEnergy_nonneg line 170
  25. theorem OAI.Thorp.Conditional.expectedEnergy_le_one line 175