OAI/Probability/ThorpShuffle/Support.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Thorp.fairMass_nonneg line 14
  2. theorem OAI.Thorp.fairMass_sum line 20
  3. theorem OAI.Thorp.sum_sub_le_tv line 27
  4. theorem OAI.Thorp.fairMass_tv_lower line 41
  5. theorem OAI.Thorp.card_position line 69
  6. theorem OAI.Thorp.card_state line 72
  7. theorem OAI.Thorp.card_coins_succ line 76
  8. theorem OAI.Thorp.card_history_succ line 79
  9. theorem OAI.Thorp.distance_support_lower line 83
  10. theorem OAI.Thorp.worst_start_eq line 92
  11. theorem OAI.Thorp.supportThreshold_le_of_distance line 109
  12. theorem OAI.Thorp.supportThreshold_le_mixingTime line 136