OAI/Combinatorics/DiscreteConvexity/FiniteProbability.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Finite probability laws

All probabilities and expectations are finite real sums. Finite laws admit elementary probability inequalities, product laws, independent samples, and uniform distributions.

  1. structure OAI.TalagrandDiscreteConvexity.FiniteLaw line 26
  2. def OAI.TalagrandDiscreteConvexity.FiniteLaw.expectation line 33
  3. def OAI.TalagrandDiscreteConvexity.FiniteLaw.prob line 36
  4. def OAI.TalagrandDiscreteConvexity.FiniteLaw.IsPositive line 40
  5. theorem OAI.TalagrandDiscreteConvexity.FiniteLaw.expectation_const line 45
  6. theorem OAI.TalagrandDiscreteConvexity.FiniteLaw.expectation_add line 49
  7. theorem OAI.TalagrandDiscreteConvexity.FiniteLaw.expectation_sub line 53
  8. theorem OAI.TalagrandDiscreteConvexity.FiniteLaw.expectation_smul line 57
  9. theorem OAI.TalagrandDiscreteConvexity.FiniteLaw.expectation_sum line 61
  10. theorem OAI.TalagrandDiscreteConvexity.FiniteLaw.expectation_nonneg line 66
  11. theorem OAI.TalagrandDiscreteConvexity.FiniteLaw.expectation_mono line 70
  12. theorem OAI.TalagrandDiscreteConvexity.FiniteLaw.prob_eq_expectation line 74
  13. theorem OAI.TalagrandDiscreteConvexity.FiniteLaw.prob_true line 79
  14. theorem OAI.TalagrandDiscreteConvexity.FiniteLaw.prob_false line 82
  15. theorem OAI.TalagrandDiscreteConvexity.FiniteLaw.prob_nonneg line 85
  16. theorem OAI.TalagrandDiscreteConvexity.FiniteLaw.prob_mono line 89
  17. theorem OAI.TalagrandDiscreteConvexity.FiniteLaw.prob_le_one line 98
  18. theorem OAI.TalagrandDiscreteConvexity.FiniteLaw.prob_compl line 101
  19. theorem OAI.TalagrandDiscreteConvexity.FiniteLaw.prob_union_le line 111
  20. theorem OAI.TalagrandDiscreteConvexity.FiniteLaw.prob_le_expectation line 119
  21. theorem OAI.TalagrandDiscreteConvexity.FiniteLaw.prob_ge_le_expectation_div line 129
  22. def OAI.TalagrandDiscreteConvexity.FiniteLaw.prod line 138
  23. theorem OAI.TalagrandDiscreteConvexity.FiniteLaw.prod_weight line 144
  24. theorem OAI.TalagrandDiscreteConvexity.FiniteLaw.expectation_prod line 147
  25. theorem OAI.TalagrandDiscreteConvexity.FiniteLaw.prod_isPositive line 151
  26. def OAI.TalagrandDiscreteConvexity.FiniteLaw.pi line 155
  27. theorem OAI.TalagrandDiscreteConvexity.FiniteLaw.pi_weight line 166
  28. def OAI.TalagrandDiscreteConvexity.FiniteLaw.iid line 170
  29. theorem OAI.TalagrandDiscreteConvexity.FiniteLaw.iid_weight line 172
  30. def OAI.TalagrandDiscreteConvexity.FiniteLaw.uniform line 175
  31. theorem OAI.TalagrandDiscreteConvexity.FiniteLaw.uniform_isPositive line 182
  32. theorem OAI.TalagrandDiscreteConvexity.FiniteLaw.uniform_prob line 185