OAI/Combinatorics/DiscreteConvexity/ProbabilisticExistence.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Extracting outcomes from a finite probability law

Normalization guarantees a positive-weight outcome. It also guarantees an outcome below the expectation and a witness to every positive-probability event; strict positivity of every individual mass is not required.

  1. theorem OAI.TalagrandDiscreteConvexity.FiniteLaw.exists_weight_pos line 19
  2. theorem OAI.TalagrandDiscreteConvexity.FiniteLaw.exists_le_expectation line 28
  3. theorem OAI.TalagrandDiscreteConvexity.FiniteLaw.exists_of_prob_pos line 44