OAI/Combinatorics/BalancedRyser/Probability/WithoutReplacementCoupling.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.WithoutReplacement.swapSet line 13
  2. theorem OAI.Balanced.WithoutReplacement.mem_swapSet line 16
  3. theorem OAI.Balanced.WithoutReplacement.card_swapSet line 20
  4. theorem OAI.Balanced.WithoutReplacement.swapSet_involutive line 24
  5. theorem OAI.Balanced.WithoutReplacement.swap_mem_iff line 29
  6. theorem OAI.Balanced.WithoutReplacement.swapSet_mem_completions_iff line 39
  7. theorem OAI.Balanced.WithoutReplacement.swapSet_eq_self_of_notMem line 61
  8. theorem OAI.Balanced.WithoutReplacement.swapSet_eq_self_of_mem line 72
  9. theorem OAI.Balanced.WithoutReplacement.swapSet_eq_exchange line 83
  10. theorem OAI.Balanced.WithoutReplacement.swapSet_insert line 95
  11. theorem OAI.Balanced.WithoutReplacement.swapSet_comm line 99
  12. theorem OAI.Balanced.WithoutReplacement.abs_sub_swapSet_le line 103
  13. def OAI.Balanced.WithoutReplacement.completionAverage line 122
  14. theorem OAI.Balanced.WithoutReplacement.completionAverage_eq_sum_div_choose line 126
  15. theorem OAI.Balanced.WithoutReplacement.completionAverage_swap line 133
  16. theorem OAI.Balanced.WithoutReplacement.completionAverage_oscillation line 144
  17. theorem OAI.Balanced.WithoutReplacement.sum_completions_eq_sum_filter line 170
  18. theorem OAI.Balanced.WithoutReplacement.sum_completions line 204
  19. theorem OAI.Balanced.WithoutReplacement.average_completion_eq line 222
  20. theorem OAI.Balanced.WithoutReplacement.completionAverage_increment line 255
  21. theorem OAI.Balanced.WithoutReplacement.completionAverage_increment_secondMoment line 269
  22. def OAI.Balanced.WithoutReplacement.finiteVariance line 281
  23. theorem OAI.Balanced.WithoutReplacement.expect_sq_sub_eq line 284
  24. theorem OAI.Balanced.WithoutReplacement.expect_sq_sub_mean_eq line 297
  25. theorem OAI.Balanced.WithoutReplacement.finiteVariance_powersetCard_le line 304