OAI/Combinatorics/BalancedRyser/Probability/PermutationHistoryLaw.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.PermutationHistoryLaw.histories line 14
  2. theorem OAI.Balanced.PermutationHistoryLaw.mem_histories line 17
  3. theorem OAI.Balanced.PermutationHistoryLaw.histories_nonempty line 21
  4. def OAI.Balanced.PermutationHistoryLaw.unused line 25
  5. theorem OAI.Balanced.PermutationHistoryLaw.next_mem_unused line 28
  6. theorem OAI.Balanced.PermutationHistoryLaw.unused_nonempty line 39
  7. theorem OAI.Balanced.PermutationHistoryLaw.card_unused line 43
  8. theorem OAI.Balanced.PermutationHistoryLaw.swap_preserves_history line 47
  9. theorem OAI.Balanced.PermutationHistoryLaw.next_fiber_card_eq line 64
  10. theorem OAI.Balanced.PermutationHistoryLaw.expect_next line 86
  11. theorem OAI.Balanced.PermutationHistoryLaw.next_probability line 99
  12. theorem OAI.Balanced.PermutationHistoryLaw.histories_card_eq line 107
  13. theorem OAI.Balanced.PermutationHistoryLaw.histories_symm line 120
  14. theorem OAI.Balanced.PermutationHistoryLaw.expect_histories line 125
  15. theorem OAI.Balanced.PermutationHistoryLaw.expect_past_next line 153
  16. theorem OAI.Balanced.PermutationHistoryLaw.map_eq_of_history line 169
  17. theorem OAI.Balanced.PermutationHistoryLaw.expect_by_image line 181
  18. theorem OAI.Balanced.PermutationHistoryLaw.uniform_measureReal_eq_expect line 197