OAI/Probability/CriticalPercolation/ProductMeasure/TailProduct.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalPercolation.BernoulliProduct.law_eq_infinitePi line 15
2. abbrev OAI.CriticalPercolation.BernoulliProduct.coordinateSigma line 20
3. abbrev OAI.CriticalPercolation.BernoulliProduct.blockSigma line 23
4. lemma OAI.CriticalPercolation.BernoulliProduct.coordinateSigma_le line 25
5. lemma OAI.CriticalPercolation.BernoulliProduct.blockSigma_le line 28
6. lemma OAI.CriticalPercolation.BernoulliProduct.independent_coordinates line 31
7. lemma OAI.CriticalPercolation.BernoulliProduct.independent_blocks line 36
8. def OAI.CriticalPercolation.BernoulliProduct.forceOn line 40
9. lemma OAI.CriticalPercolation.BernoulliProduct.measurable_forceOn_block line 42
10. lemma OAI.CriticalPercolation.BernoulliProduct.measurable_forceOn line 55
11. theorem OAI.CriticalPercolation.BernoulliProduct.zero_one_of_finite_erasure_invariant line 58