OAI/Probability/CriticalPercolation/ProductMeasure/FiniteProductPin.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.FiniteProduct.pin line 18
2. lemma OAI.CriticalPercolation.FiniteProduct.pin_nonneg line 22
3. lemma OAI.CriticalPercolation.FiniteProduct.pin_normalized line 30
4. lemma OAI.CriticalPercolation.FiniteProduct.density_pin line 38
5. lemma OAI.CriticalPercolation.FiniteProduct.expect_mask_pin line 51
6. def OAI.CriticalPercolation.FiniteProduct.prefixEvent line 65
7. def OAI.CriticalPercolation.FiniteProduct.prefixWeight line 69
8. def OAI.CriticalPercolation.FiniteProduct.prefixFactor line 73
9. lemma OAI.CriticalPercolation.FiniteProduct.prefixWeight_nonneg line 78
10. lemma OAI.CriticalPercolation.FiniteProduct.prefixWeight_normalized line 85
11. lemma OAI.CriticalPercolation.FiniteProduct.prefixFactor_nonneg line 92
12. theorem OAI.CriticalPercolation.FiniteProduct.expect_prefix line 98
13. lemma OAI.CriticalPercolation.FiniteProduct.prefixWeight_fresh line 112