OAI/Probability/ThorpShuffle/TaggedCompletion.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Thorp.Conditional.freeOf line 16
  2. theorem OAI.Thorp.Conditional.freeOf_exposed line 19
  3. theorem OAI.Thorp.Conditional.freeOf_true line 23
  4. theorem OAI.Thorp.Conditional.freeOf_perm line 27
  5. theorem OAI.Thorp.Conditional.freeCount_perm line 32
  6. theorem OAI.Thorp.Conditional.freeCount_freeOf line 39
  7. def OAI.Thorp.Conditional.completeTest line 48
  8. theorem OAI.Thorp.Conditional.completeTest_bound line 52
  9. theorem OAI.Thorp.Conditional.uniform_tagged_completion line 72