OAI/Probability/CriticalPercolation/Criticality/BlockIndependence.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalPercolation.BernoulliProduct.blockSigma_mono line 15
2. lemma OAI.CriticalPercolation.BernoulliProduct.independent_disjoint_blocks line 20
3. theorem OAI.CriticalPercolation.BernoulliProduct.independent_block_family line 24
4. lemma OAI.CriticalPercolation.BernoulliProduct.independent_block_events line 51
5. def OAI.CriticalPercolation.BernoulliProduct.closedBlock line 57
6. lemma OAI.CriticalPercolation.BernoulliProduct.measurableSet_closed_coordinate line 59
7. lemma OAI.CriticalPercolation.BernoulliProduct.measurableSet_closedBlock line 70
8. lemma OAI.CriticalPercolation.BernoulliProduct.law_closedBlock line 81
9. lemma OAI.CriticalPercolation.BernoulliProduct.law_closedBlock_const line 97