OAI/Probability/CriticalPercolation/ProductMeasure/Prob.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.FiniteProduct.prob line 17
2. lemma OAI.CriticalPercolation.FiniteProduct.prob_nonneg line 20
3. lemma OAI.CriticalPercolation.FiniteProduct.prob_mono line 23
4. lemma OAI.CriticalPercolation.FiniteProduct.prob_split line 30
5. lemma OAI.CriticalPercolation.FiniteProduct.prob_congr line 38
6. lemma OAI.CriticalPercolation.FiniteProduct.indicator_mask line 44
7. lemma OAI.CriticalPercolation.FiniteProduct.indicator_mask_mul line 48
8. lemma OAI.CriticalPercolation.FiniteProduct.indicator_antitone line 53
9. lemma OAI.CriticalPercolation.FiniteProduct.indicator_monotone line 60
10. lemma OAI.CriticalPercolation.FiniteProduct.expect_mul_ge_antitone line 67
11. lemma OAI.CriticalPercolation.FiniteProduct.prob_harris_decreasing line 76