OAI/Probability/CriticalPercolation/ProductMeasure/Density.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.FiniteProduct.density line 14
2. def OAI.CriticalPercolation.FiniteProduct.expect line 16
3. lemma OAI.CriticalPercolation.FiniteProduct.density_nonneg line 21
4. lemma OAI.CriticalPercolation.FiniteProduct.sum_density line 24
5. lemma OAI.CriticalPercolation.FiniteProduct.expect_const line 31
6. lemma OAI.CriticalPercolation.FiniteProduct.expect_add line 36
7. lemma OAI.CriticalPercolation.FiniteProduct.expect_sub line 41
8. lemma OAI.CriticalPercolation.FiniteProduct.expect_mono line 46
9. lemma OAI.CriticalPercolation.FiniteProduct.density_split line 52
10. lemma OAI.CriticalPercolation.FiniteProduct.expect_split line 58
11. lemma OAI.CriticalPercolation.FiniteProduct.expect_factor line 80
12. lemma OAI.CriticalPercolation.FiniteProduct.expect_indep line 107
13. lemma OAI.CriticalPercolation.FiniteProduct.expect_mul_const line 132
14. lemma OAI.CriticalPercolation.FiniteProduct.expect_partition line 141
15. lemma OAI.CriticalPercolation.FiniteProduct.expect_exposure line 153