OAI/Combinatorics/GraphThreshold/FiniteProbability.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LeanBlast.SecondKahnKalai.FiniteLaw.expectation_const line 23
  2. theorem OAI.LeanBlast.SecondKahnKalai.FiniteLaw.expectation_add line 27
  3. theorem OAI.LeanBlast.SecondKahnKalai.FiniteLaw.expectation_sub line 31
  4. theorem OAI.LeanBlast.SecondKahnKalai.FiniteLaw.expectation_smul line 35
  5. theorem OAI.LeanBlast.SecondKahnKalai.FiniteLaw.expectation_sum line 39
  6. theorem OAI.LeanBlast.SecondKahnKalai.FiniteLaw.expectation_nonneg line 44
  7. theorem OAI.LeanBlast.SecondKahnKalai.FiniteLaw.expectation_mono line 48
  8. theorem OAI.LeanBlast.SecondKahnKalai.FiniteLaw.prob_eq_expectation line 52
  9. theorem OAI.LeanBlast.SecondKahnKalai.FiniteLaw.prob_true line 57
  10. theorem OAI.LeanBlast.SecondKahnKalai.FiniteLaw.prob_false line 60
  11. theorem OAI.LeanBlast.SecondKahnKalai.FiniteLaw.prob_nonneg line 63
  12. theorem OAI.LeanBlast.SecondKahnKalai.FiniteLaw.prob_mono line 67
  13. theorem OAI.LeanBlast.SecondKahnKalai.FiniteLaw.prob_le_one line 76
  14. theorem OAI.LeanBlast.SecondKahnKalai.FiniteLaw.prob_compl line 79
  15. theorem OAI.LeanBlast.SecondKahnKalai.FiniteLaw.prob_union_le line 89
  16. theorem OAI.LeanBlast.SecondKahnKalai.FiniteLaw.prob_le_expectation line 97
  17. theorem OAI.LeanBlast.SecondKahnKalai.FiniteLaw.prob_ge_le_expectation_div line 107
  18. def OAI.LeanBlast.SecondKahnKalai.FiniteLaw.prod line 116
  19. theorem OAI.LeanBlast.SecondKahnKalai.FiniteLaw.prod_weight line 122
  20. theorem OAI.LeanBlast.SecondKahnKalai.FiniteLaw.expectation_prod line 125
  21. theorem OAI.LeanBlast.SecondKahnKalai.FiniteLaw.prod_isPositive line 129
  22. def OAI.LeanBlast.SecondKahnKalai.FiniteLaw.pi line 133
  23. theorem OAI.LeanBlast.SecondKahnKalai.FiniteLaw.pi_weight line 144
  24. def OAI.LeanBlast.SecondKahnKalai.FiniteLaw.iid line 148
  25. theorem OAI.LeanBlast.SecondKahnKalai.FiniteLaw.iid_weight line 150
  26. def OAI.LeanBlast.SecondKahnKalai.FiniteLaw.uniform line 153
  27. theorem OAI.LeanBlast.SecondKahnKalai.FiniteLaw.uniform_isPositive line 160
  28. theorem OAI.LeanBlast.SecondKahnKalai.FiniteLaw.uniform_prob line 163
  29. def OAI.LeanBlast.SecondKahnKalai.finsetBoolEquiv line 171
  30. theorem OAI.LeanBlast.SecondKahnKalai.sum_finset_product line 179
  31. theorem OAI.LeanBlast.SecondKahnKalai.bernoulliExpectation_product line 188
  32. theorem OAI.LeanBlast.SecondKahnKalai.bernoulliWeight_nonneg line 195
  33. theorem OAI.LeanBlast.SecondKahnKalai.bernoulliWeight_pos line 201
  34. theorem OAI.LeanBlast.SecondKahnKalai.bernoulliWeight_sum line 207
  35. def OAI.LeanBlast.SecondKahnKalai.bernoulliLaw line 212
  36. theorem OAI.LeanBlast.SecondKahnKalai.bernoulliLaw_weight line 217
  37. theorem OAI.LeanBlast.SecondKahnKalai.bernoulliLaw_expectation line 220
  38. theorem OAI.LeanBlast.SecondKahnKalai.bernoulliLaw_prob line 224
  39. theorem OAI.LeanBlast.SecondKahnKalai.bernoulliProbability_eq_expectation line 227
  40. theorem OAI.LeanBlast.SecondKahnKalai.subset_indicator_product line 232
  41. theorem OAI.LeanBlast.SecondKahnKalai.bernoulliProbability_subset line 238