OAI/Probability/CriticalPercolation/Criticality/BlockLocalization.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalPercolation.BondGraph.finset_weight_lower line 19
2. lemma OAI.CriticalPercolation.BondGraph.cluster_subset_ball_of_mass line 31
3. lemma OAI.CriticalPercolation.BondGraph.cluster_eq_of_incident_agree line 58
4. lemma OAI.CriticalPercolation.BondGraph.freshClusterBoundary_subset_incident line 66
5. lemma OAI.CriticalPercolation.BondGraph.boundedDomainFreshExit_of_agree line 71
6. lemma OAI.CriticalPercolation.BondGraph.dependsOn_boundedDomainFreshExit line 98