OAI/Combinatorics/DiscreteConvexity/Bernoulli.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

Bernoulli product laws and Boolean cubes

The algebraic identities hold for every real parameter. Nonnegative normalized laws additionally require a parameter in the closed unit interval.

  1. def OAI.TalagrandDiscreteConvexity.bitWeight line 23

    Source documentation

    The mass of a Bernoulli bit.

    def bitWeight (p : ℝ) (b : Bool) : ℝ := if b then p else 1 - p

    Mentions: OAI.TalagrandDiscreteConvexity.b

  2. theorem OAI.TalagrandDiscreteConvexity.bitWeight_true line 25
  3. theorem OAI.TalagrandDiscreteConvexity.bitWeight_false line 26
  4. theorem OAI.TalagrandDiscreteConvexity.bitWeight_nonneg line 28
  5. def OAI.TalagrandDiscreteConvexity.bitLaw line 34
  6. theorem OAI.TalagrandDiscreteConvexity.bitLaw_weight line 39
  7. theorem OAI.TalagrandDiscreteConvexity.bitLaw_prob_true line 42
  8. theorem OAI.TalagrandDiscreteConvexity.bitLaw_prob_false line 46
  9. def OAI.TalagrandDiscreteConvexity.cubeWeight line 53

    Source documentation

    Product mass on the Boolean cube, including signed parameters.

    def cubeWeight (p : ℝ) (x : α → Bool) : ℝ := ∏ i, bitWeight p (x i)

    Mentions: OAI.TalagrandDiscreteConvexity.bitWeight

  10. def OAI.TalagrandDiscreteConvexity.cubeExpectation line 55
  11. def OAI.TalagrandDiscreteConvexity.bernoulliWeight line 58
  12. def OAI.TalagrandDiscreteConvexity.bernoulliExpectation line 61
  13. def OAI.TalagrandDiscreteConvexity.bernoulliProbability line 64
  14. def OAI.TalagrandDiscreteConvexity.finsetBoolEquiv line 67
  15. theorem OAI.TalagrandDiscreteConvexity.sum_finset_product line 75
  16. theorem OAI.TalagrandDiscreteConvexity.bernoulliExpectation_product line 84
  17. theorem OAI.TalagrandDiscreteConvexity.bernoulliWeight_nonneg line 91
  18. theorem OAI.TalagrandDiscreteConvexity.bernoulliWeight_pos line 97
  19. theorem OAI.TalagrandDiscreteConvexity.bernoulliWeight_sum line 103
  20. def OAI.TalagrandDiscreteConvexity.bernoulliLaw line 108
  21. theorem OAI.TalagrandDiscreteConvexity.bernoulliLaw_weight line 113
  22. theorem OAI.TalagrandDiscreteConvexity.bernoulliLaw_expectation line 116
  23. theorem OAI.TalagrandDiscreteConvexity.bernoulliLaw_prob line 120
  24. theorem OAI.TalagrandDiscreteConvexity.bernoulliProbability_eq_expectation line 123
  25. theorem OAI.TalagrandDiscreteConvexity.subset_indicator_product line 128
  26. theorem OAI.TalagrandDiscreteConvexity.bernoulliProbability_subset line 134
  27. theorem OAI.TalagrandDiscreteConvexity.bernoulliWeight_eq_mass line 165
  28. theorem OAI.TalagrandDiscreteConvexity.cubeSet_finsetBoolEquiv line 171
  29. theorem OAI.TalagrandDiscreteConvexity.cubeWeight_finsetBoolEquiv line 174
  30. theorem OAI.TalagrandDiscreteConvexity.cubeWeight_nonneg line 179
  31. theorem OAI.TalagrandDiscreteConvexity.cubeWeight_sum line 183
  32. theorem OAI.TalagrandDiscreteConvexity.cubeExpectation_eq_bernoulliExpectation line 187
  33. theorem OAI.TalagrandDiscreteConvexity.cubeExpectation_product line 193
  34. theorem OAI.TalagrandDiscreteConvexity.cubeExpectation_familyIndicator line 199
  35. theorem OAI.TalagrandDiscreteConvexity.bernoulliLaw_prob_subset line 207
  36. theorem OAI.TalagrandDiscreteConvexity.bernoulliLaw_prob_mem line 212
  37. theorem OAI.TalagrandDiscreteConvexity.disjoint_indicator_product line 216
  38. theorem OAI.TalagrandDiscreteConvexity.bernoulliProbability_disjoint line 236
  39. theorem OAI.TalagrandDiscreteConvexity.bernoulliLaw_prob_disjoint line 259
  40. theorem OAI.TalagrandDiscreteConvexity.bernoulliLaw_expect_sum_mem line 264