OAI/Probability/CriticalPercolation/Criticality/DomainPercolation.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.BondGraph.domainInfiniteEvent line 19
2. def OAI.CriticalPercolation.BondGraph.domainHitEvent line 22
3. lemma OAI.CriticalPercolation.BondGraph.measurableSet_domainInfiniteEvent line 25
4. lemma OAI.CriticalPercolation.BondGraph.domainInfiniteEvent_mono line 30
5. lemma OAI.CriticalPercolation.BondGraph.walk_finite_bond_witness line 35
6. lemma OAI.CriticalPercolation.BondGraph.InsideWalk.domainHit_lower line 56
7. lemma OAI.CriticalPercolation.BondGraph.domainInfinite_transfer line 72
8. lemma OAI.CriticalPercolation.BondGraph.InsideWalk.domainInfinite_lower line 91
9. lemma OAI.CriticalPercolation.BondGraph.bounded_mass_infinite_subset_domain line 99
10. lemma OAI.CriticalPercolation.BondGraph.real_domainInfinite_ceiling_lower line 107
11. theorem OAI.CriticalPercolation.BondGraph.uniform_safeDomain_percolation line 118