OAI/Combinatorics/GraphThreshold/BernoulliUnion.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LeanBlast.SecondKahnKalai.bernoulli_union_product line 15
2. theorem OAI.LeanBlast.SecondKahnKalai.bernoulli_union_mass line 41
3. theorem OAI.LeanBlast.SecondKahnKalai.bernoulliExpectation_union line 59

   Source documentation

   The union of two independent Bernoulli subsets has the stated Bernoulli law.

   theorem bernoulliExpectation_union (p q : ℝ) (F : Finset X → ℝ) :
       bernoulliExpectation p (fun U => bernoulliExpectation q (fun V => F (U ∪ V))) =
         bernoulliExpectation (p + q - p * q) F := by
   …

   Mentions: OAI.LeanBlast.SecondKahnKalai.bernoulliExpectation

4. theorem OAI.LeanBlast.SecondKahnKalai.biUnion_fin_cons line 82
5. theorem OAI.LeanBlast.SecondKahnKalai.iid_bernoulli_union_expectation line 99

   Source documentation

   Exact law of the union of a finite history of independent draws.

   theorem iid_bernoulli_union_expectation (p : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1)
       (n : ℕ) (F : Finset X → ℝ) :
       ((bernoulliLaw p hp0 hp1).iid n).expectation (fun draws => F (Finset.univ.biUnion draws)) =
         bernoulliExpectation (1 - (1 - p) ^ n) F := by
   …

   Mentions: OAI.LeanBlast.SecondKahnKalai.bernoulliLaw, OAI.LeanBlast.SecondKahnKalai.bernoulliExpectation

6. theorem OAI.LeanBlast.SecondKahnKalai.iid_bernoulli_union_probability line 119
7. theorem OAI.LeanBlast.SecondKahnKalai.bernoulli_union_parameter_mem line 126
8. theorem OAI.LeanBlast.SecondKahnKalai.bernoulli_union_parameter_le line 132