OAI/Probability/CriticalPercolation/Criticality/WitnessEvents.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalPercolation.BernoulliProduct.tendsto_real_inter_finiteWitness line 17
2. def OAI.CriticalPercolation.BondGraph.witnessedTwoCluster line 32
3. lemma OAI.CriticalPercolation.BondGraph.witnessedTwoCluster_subset_restrict line 36
4. lemma OAI.CriticalPercolation.BondGraph.measurableSet_witnessedTwoCluster line 44
5. lemma OAI.CriticalPercolation.BondGraph.tendsto_real_witnessedTwoCluster line 50
6. lemma OAI.CriticalPercolation.BondGraph.exists_finite_witnessedTwoCluster line 62
7. lemma OAI.CriticalPercolation.BondGraph.Aut.reachable_map line 72
8. lemma OAI.CriticalPercolation.BondGraph.Aut.clusterTail_map line 77
9. lemma OAI.CriticalPercolation.BondGraph.Aut.witnessedTwoCluster_preimage line 81
10. lemma OAI.CriticalPercolation.BondGraph.Aut.witnessedTwoCluster_real line 90
11. lemma OAI.CriticalPercolation.BondGraph.twoClusterEvent_comm line 101
12. lemma OAI.CriticalPercolation.BondGraph.twoClusterEvent_sym2 line 111