OAI/Combinatorics/Ryser/Probability/Finite.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.RyserCoveringCounterexample.FiniteLaw line 18
  2. def OAI.RyserCoveringCounterexample.FiniteLaw.expectation line 25
  3. def OAI.RyserCoveringCounterexample.FiniteLaw.prob line 28
  4. def OAI.RyserCoveringCounterexample.FiniteLaw.IsPositive line 32
  5. theorem OAI.RyserCoveringCounterexample.FiniteLaw.expectation_const line 37
  6. theorem OAI.RyserCoveringCounterexample.FiniteLaw.expectation_add line 41
  7. theorem OAI.RyserCoveringCounterexample.FiniteLaw.expectation_sub line 45
  8. theorem OAI.RyserCoveringCounterexample.FiniteLaw.expectation_smul line 49
  9. theorem OAI.RyserCoveringCounterexample.FiniteLaw.expectation_sum line 53
  10. theorem OAI.RyserCoveringCounterexample.FiniteLaw.expectation_nonneg line 58
  11. theorem OAI.RyserCoveringCounterexample.FiniteLaw.expectation_mono line 62
  12. theorem OAI.RyserCoveringCounterexample.FiniteLaw.prob_eq_expectation line 66
  13. theorem OAI.RyserCoveringCounterexample.FiniteLaw.prob_true line 71
  14. theorem OAI.RyserCoveringCounterexample.FiniteLaw.prob_false line 74
  15. theorem OAI.RyserCoveringCounterexample.FiniteLaw.prob_nonneg line 77
  16. theorem OAI.RyserCoveringCounterexample.FiniteLaw.prob_mono line 81
  17. theorem OAI.RyserCoveringCounterexample.FiniteLaw.prob_le_one line 90
  18. theorem OAI.RyserCoveringCounterexample.FiniteLaw.prob_compl line 93
  19. theorem OAI.RyserCoveringCounterexample.FiniteLaw.prob_union_le line 103
  20. theorem OAI.RyserCoveringCounterexample.FiniteLaw.prob_le_expectation line 111
  21. theorem OAI.RyserCoveringCounterexample.FiniteLaw.prob_ge_le_expectation_div line 121
  22. def OAI.RyserCoveringCounterexample.FiniteLaw.prod line 130
  23. theorem OAI.RyserCoveringCounterexample.FiniteLaw.prod_weight line 136
  24. theorem OAI.RyserCoveringCounterexample.FiniteLaw.expectation_prod line 139
  25. theorem OAI.RyserCoveringCounterexample.FiniteLaw.prod_isPositive line 143
  26. def OAI.RyserCoveringCounterexample.FiniteLaw.pi line 147
  27. theorem OAI.RyserCoveringCounterexample.FiniteLaw.pi_weight line 158
  28. def OAI.RyserCoveringCounterexample.FiniteLaw.iid line 162
  29. theorem OAI.RyserCoveringCounterexample.FiniteLaw.iid_weight line 164
  30. def OAI.RyserCoveringCounterexample.FiniteLaw.uniform line 167
  31. theorem OAI.RyserCoveringCounterexample.FiniteLaw.uniform_isPositive line 174
  32. theorem OAI.RyserCoveringCounterexample.FiniteLaw.uniform_prob line 177
  33. theorem OAI.RyserCoveringCounterexample.FiniteLaw.ext_weight line 181
  34. theorem OAI.RyserCoveringCounterexample.FiniteLaw.eq_uniform_of_weight_eq line 188
  35. theorem OAI.RyserCoveringCounterexample.FiniteLaw.uniform_expectation line 206
  36. theorem OAI.RyserCoveringCounterexample.FiniteLaw.prob_exists_le line 211