OAI/Combinatorics/GraphThreshold/BernoulliCoupling.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LeanBlast.SecondKahnKalai.bernoulliExpectation_congr line 15
2. theorem OAI.LeanBlast.SecondKahnKalai.bernoulliExpectation_const line 19
3. theorem OAI.LeanBlast.SecondKahnKalai.bernoulliExpectation_add line 23
4. theorem OAI.LeanBlast.SecondKahnKalai.bernoulliExpectation_smul line 28
5. theorem OAI.LeanBlast.SecondKahnKalai.bernoulliExpectation_sum line 32
6. theorem OAI.LeanBlast.SecondKahnKalai.bernoulliExpectation_nonneg line 38
7. theorem OAI.LeanBlast.SecondKahnKalai.bernoulliExpectation_mono line 42
8. theorem OAI.LeanBlast.SecondKahnKalai.finset_eq_indicator_product line 47
9. theorem OAI.LeanBlast.SecondKahnKalai.bernoulliExpectation_pushforward line 55
10. theorem OAI.LeanBlast.SecondKahnKalai.bernoulli_union_fixed_mass line 71
11. theorem OAI.LeanBlast.SecondKahnKalai.bernoulli_union_fixed_mass_mul line 86
12. theorem OAI.LeanBlast.SecondKahnKalai.bernoulli_union_fixed_mass_div line 109
13. theorem OAI.LeanBlast.SecondKahnKalai.bernoulliExpectation_union_fixed line 117

    Source documentation

    Forcing all coordinates of A to be present gives the literal Bernoulli law conditioned on containing A.

    theorem bernoulliExpectation_union_fixed (p : ℝ) (hp : p ≠ 0)
        (A : Finset X) (F : Finset X → ℝ) :
        bernoulliExpectation p (fun W => F (W ∪ A)) =
          bernoulliExpectation p (fun Y => if A ⊆ Y then F Y / p ^ A.card else 0) := by
    …

    Mentions: OAI.LeanBlast.SecondKahnKalai.bernoulliExpectation