BernoulliMonotonicity.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Monotonicity of finite Bernoulli probabilities

For p ≤ q, adjoin an independent Bernoulli set to a Bernoulli-p set. The resulting union has parameter q and contains the first set. This gives expectation and event monotonicity, including both endpoints of [0, 1].

theorem OAI.LeanBlast.SecondKahnKalai.bernoulliExpectation_mono_parameter line 22
Source documentation
A Bernoulli set with a larger parameter has larger expectation for every function monotone under inclusion. The function need not be nonnegative.
```
theorem bernoulliExpectation_mono_parameter {p q : ℝ}
    (hp0 : 0 ≤ p) (hpq : p ≤ q) (hq1 : q ≤ 1) (F : Finset X → ℝ)
    (hF : ∀ U V, U ⊆ V → F U ≤ F V) :
    bernoulliExpectation p F ≤ bernoulliExpectation q F := by
…
```
Mentions: OAI.LeanBlast.SecondKahnKalai.bernoulliExpectation
theorem OAI.LeanBlast.SecondKahnKalai.bernoulliProbability_mono_parameter line 54
Source documentation
Inclusion-monotone events become more likely as the Bernoulli parameter increases. The proof couples actual independent finite Bernoulli sets.
```
theorem bernoulliProbability_mono_parameter {p q : ℝ}
    (hp0 : 0 ≤ p) (hpq : p ≤ q) (hq1 : q ≤ 1) (P : Finset X → Prop)
    (hP : ∀ U V, U ⊆ V → P U → P V) :
    bernoulliProbability p P ≤ bernoulliProbability q P := by
…
```
Mentions: OAI.LeanBlast.SecondKahnKalai.bernoulliProbability