OAI/Probability/CriticalPercolation/ProductMeasure/MonotoneBernoulli.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalPercolation.BernoulliProduct.uniform01_map_threshold line 14
2. def OAI.CriticalPercolation.BernoulliProduct.markLaw line 43
3. instance OAI.CriticalPercolation.BernoulliProduct.(instance at line 45) line 45
4. def OAI.CriticalPercolation.BernoulliProduct.atParameter line 49
5. lemma OAI.CriticalPercolation.BernoulliProduct.measurable_atParameter line 51
6. lemma OAI.CriticalPercolation.BernoulliProduct.markLaw_map_atParameter line 54
7. lemma OAI.CriticalPercolation.BernoulliProduct.atParameter_mono line 63
8. lemma OAI.CriticalPercolation.BernoulliProduct.atParameter_iUnion line 66
9. def OAI.CriticalPercolation.BernoulliProduct.reindexMarks line 78
10. lemma OAI.CriticalPercolation.BernoulliProduct.measurable_reindexMarks line 80
11. lemma OAI.CriticalPercolation.BernoulliProduct.markLaw_map_reindex line 83
12. lemma OAI.CriticalPercolation.BernoulliProduct.atParameter_reindex line 92