OAI/Combinatorics/ExpectationThreshold/ProbabilityFinite.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Finite probability laws

Probabilities and expectations are finite real sums. Independent samples, product laws, and uniform laws satisfy the usual elementary inequalities.

  1. structure OAI.TalagrandThreshold.FiniteLaw line 25
  2. def OAI.TalagrandThreshold.FiniteLaw.expectation line 32
  3. def OAI.TalagrandThreshold.FiniteLaw.prob line 35
  4. def OAI.TalagrandThreshold.FiniteLaw.IsPositive line 39
  5. theorem OAI.TalagrandThreshold.FiniteLaw.expectation_const line 44
  6. theorem OAI.TalagrandThreshold.FiniteLaw.expectation_add line 48
  7. theorem OAI.TalagrandThreshold.FiniteLaw.expectation_sub line 52
  8. theorem OAI.TalagrandThreshold.FiniteLaw.expectation_smul line 56
  9. theorem OAI.TalagrandThreshold.FiniteLaw.expectation_sum line 60
  10. theorem OAI.TalagrandThreshold.FiniteLaw.expectation_nonneg line 65
  11. theorem OAI.TalagrandThreshold.FiniteLaw.expectation_mono line 69
  12. theorem OAI.TalagrandThreshold.FiniteLaw.prob_eq_expectation line 73
  13. theorem OAI.TalagrandThreshold.FiniteLaw.prob_true line 78
  14. theorem OAI.TalagrandThreshold.FiniteLaw.prob_false line 81
  15. theorem OAI.TalagrandThreshold.FiniteLaw.prob_nonneg line 84
  16. theorem OAI.TalagrandThreshold.FiniteLaw.prob_mono line 88
  17. theorem OAI.TalagrandThreshold.FiniteLaw.prob_le_one line 97
  18. theorem OAI.TalagrandThreshold.FiniteLaw.prob_compl line 100
  19. theorem OAI.TalagrandThreshold.FiniteLaw.prob_union_le line 110
  20. theorem OAI.TalagrandThreshold.FiniteLaw.prob_le_expectation line 118
  21. theorem OAI.TalagrandThreshold.FiniteLaw.prob_ge_le_expectation_div line 128
  22. def OAI.TalagrandThreshold.FiniteLaw.prod line 137
  23. theorem OAI.TalagrandThreshold.FiniteLaw.prod_weight line 143
  24. theorem OAI.TalagrandThreshold.FiniteLaw.expectation_prod line 146
  25. theorem OAI.TalagrandThreshold.FiniteLaw.prod_isPositive line 150
  26. def OAI.TalagrandThreshold.FiniteLaw.pi line 154
  27. theorem OAI.TalagrandThreshold.FiniteLaw.pi_weight line 165
  28. def OAI.TalagrandThreshold.FiniteLaw.iid line 169
  29. theorem OAI.TalagrandThreshold.FiniteLaw.iid_weight line 171
  30. def OAI.TalagrandThreshold.FiniteLaw.uniform line 174
  31. theorem OAI.TalagrandThreshold.FiniteLaw.uniform_isPositive line 181
  32. theorem OAI.TalagrandThreshold.FiniteLaw.uniform_prob line 184