OAI/Probability/CriticalPercolation/ProductMeasure/Distribution.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalPercolation.FiniteProduct.expect_zero line 15
2. lemma OAI.CriticalPercolation.FiniteProduct.expect_sum line 18
3. lemma OAI.CriticalPercolation.FiniteProduct.expect_nonneg line 25
4. def OAI.CriticalPercolation.FiniteProduct.distribution line 30
5. lemma OAI.CriticalPercolation.FiniteProduct.expect_comp line 34
6. lemma OAI.CriticalPercolation.FiniteProduct.distribution_nonneg line 43
7. lemma OAI.CriticalPercolation.FiniteProduct.distribution_mass line 48
8. lemma OAI.CriticalPercolation.FiniteProduct.expect_const_mul line 57