OAI/Probability/CriticalPercolation/ProductMeasure/BitMeasure.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.BernoulliProduct.bitMeasure line 15
2. instance OAI.CriticalPercolation.BernoulliProduct.bitMeasure_probability line 19
3. def OAI.CriticalPercolation.BernoulliProduct.bitWeight line 23
4. lemma OAI.CriticalPercolation.BernoulliProduct.bitWeight_sum line 26
5. lemma OAI.CriticalPercolation.BernoulliProduct.bitWeight_nonneg line 29
6. lemma OAI.CriticalPercolation.BernoulliProduct.bitMeasure_real_singleton line 35
7. def OAI.CriticalPercolation.BernoulliProduct.law line 47
8. instance OAI.CriticalPercolation.BernoulliProduct.law_probability line 50
9. lemma OAI.CriticalPercolation.BernoulliProduct.law_const line 54
10. lemma OAI.CriticalPercolation.BernoulliProduct.integral_bits_eq_expect line 59
11. lemma OAI.CriticalPercolation.BernoulliProduct.integral_law_eq_expect line 71
12. lemma OAI.CriticalPercolation.BernoulliProduct.law_map_restrict line 78