OAI/Probability/CriticalPercolation/Modular/ClusterTransportGeometry.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.FiniteClusters.small line 15
2. lemma OAI.CriticalPercolation.FiniteClusters.small_cluster_subset line 18
3. lemma OAI.CriticalPercolation.FiniteClusters.small_finite line 22
4. lemma OAI.CriticalPercolation.FiniteClusters.small_mono line 26
5. lemma OAI.CriticalPercolation.FiniteClusters.small_reachable line 30
6. lemma OAI.CriticalPercolation.FiniteClusters.eventually_small line 35
7. lemma OAI.CriticalPercolation.FiniteClusters.small_aut line 42
8. lemma OAI.CriticalPercolation.FiniteClusters.mass_aut line 52
9. lemma OAI.CriticalPercolation.FiniteClusters.coefficient_aut line 57
10. lemma OAI.CriticalPercolation.FiniteClusters.incidentCluster_aut line 61
11. lemma OAI.CriticalPercolation.FiniteClusters.incidentRoots line 72
12. lemma OAI.CriticalPercolation.FiniteClusters.measurable_small line 90