OAI/Probability/CriticalPercolation/ProductMeasure/FiniteOpenWitness.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalPercolation.BernoulliProduct.continuous_bitWeight line 22
2. lemma OAI.CriticalPercolation.BernoulliProduct.continuous_real_law_finite line 28
3. lemma OAI.CriticalPercolation.BernoulliProduct.real_law_restrict line 40
4. lemma OAI.CriticalPercolation.BernoulliProduct.continuous_real_law_restrict line 55
5. def OAI.CriticalPercolation.BernoulliProduct.HasFiniteOpenWitness line 62
6. lemma OAI.CriticalPercolation.BernoulliProduct.finiteWitness_exhaustion line 65
7. lemma OAI.CriticalPercolation.BernoulliProduct.finiteWitness_exhaustion_mono line 78
8. lemma OAI.CriticalPercolation.BernoulliProduct.tendsto_real_finiteWitness line 84
9. lemma OAI.CriticalPercolation.BernoulliProduct.lowerSemicontinuous_real_finiteWitness line 94
10. lemma OAI.CriticalPercolation.BernoulliProduct.exists_lower_parameter line 105