OAI/Probability/CriticalPercolation/ProductMeasure/FiniteInterpolationMeasure.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalPercolation.BernoulliProduct.prob_eq_real line 18
2. def OAI.CriticalPercolation.BondGraph.twoClusterEvent line 28
3. lemma OAI.CriticalPercolation.BondGraph.measurableSet_twoClusterEvent line 31
4. lemma OAI.CriticalPercolation.BondGraph.clusterTail_iff_card line 36
5. lemma OAI.CriticalPercolation.BondGraph.twoClusterEvent_iff_endpoint line 44
6. lemma OAI.CriticalPercolation.BondGraph.finite_endpoint_prob line 49
7. theorem OAI.CriticalPercolation.BondGraph.finite_interpolation_measure line 57