OAI/Probability/CriticalPercolation/ProductMeasure/Potential.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalPercolation.FiniteVariance.sq_div_le_self line 16
2. lemma OAI.CriticalPercolation.FiniteVariance.binary_split line 24
3. lemma OAI.CriticalPercolation.FiniteProduct.expect_prop_mask_pin line 44
4. lemma OAI.CriticalPercolation.FiniteProduct.expect_split_pin line 51
5. lemma OAI.CriticalPercolation.FiniteProduct.expect_congr_support line 72
6. lemma OAI.CriticalPercolation.FiniteProduct.density_pin_support line 81
7. lemma OAI.CriticalPercolation.FiniteProduct.density_pin_old_support line 87
8. lemma OAI.CriticalPercolation.FiniteProduct.expect_pin_mask line 94
9. def OAI.CriticalPercolation.FiniteProduct.potential line 101
10. lemma OAI.CriticalPercolation.FiniteProduct.potential_le line 104
11. lemma OAI.CriticalPercolation.FiniteProduct.potential_nonneg line 110
12. lemma OAI.CriticalPercolation.FiniteProduct.potential_split line 116