OAI/Probability/ThorpShuffle/BlockFibers.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Thorp.Block.fiberEquiv line 18
  2. lemma OAI.Thorp.Block.push_restriction line 26
  3. lemma OAI.Thorp.Block.push_uniform_restriction line 38
  4. def OAI.Thorp.Block.orderedRestriction line 47
  5. lemma OAI.Thorp.Block.orderedRestriction_eq_iff line 51
  6. lemma OAI.Thorp.Block.push_orderedRestriction line 64
  7. lemma OAI.Thorp.Block.uniform_orderedRestriction line 79
  8. lemma OAI.Thorp.Block.discarded_ordered_bound line 87
  9. lemma OAI.Thorp.law_nonneg line 99
  10. lemma OAI.Thorp.law_sum line 101
  11. def OAI.Thorp.Block.eightEquiv line 106
  12. lemma OAI.Thorp.Block.complement_card line 109
  13. def OAI.Thorp.Block.ordering line 113
  14. def OAI.Thorp.Block.domain line 116
  15. lemma OAI.Thorp.Block.domain_injective line 119
  16. lemma OAI.Thorp.Block.push_law_ordered line 122
  17. lemma OAI.Thorp.Block.push_uniform_ordered line 128
  18. def OAI.Thorp.Block.discarded line 136
  19. lemma OAI.Thorp.Block.discarded_nonneg line 139
  20. lemma OAI.Thorp.Block.discarded_le line 142
  21. lemma OAI.Thorp.Block.discarded_tendsto line 151