OAI/Probability/CriticalPercolation/Modular/ClusterMassRestriction.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalPercolation.FiniteClusters.cluster_inter_eq line 15
2. lemma OAI.CriticalPercolation.FiniteClusters.restrict_cluster line 29
3. lemma OAI.CriticalPercolation.FiniteClusters.restrict_incident line 33
4. lemma OAI.CriticalPercolation.FiniteClusters.restrict_local line 36
5. lemma OAI.CriticalPercolation.FiniteClusters.restrict_incident_bound line 41
6. lemma OAI.CriticalPercolation.FiniteClusters.restrict_rootSum_eq line 48
7. lemma OAI.CriticalPercolation.FiniteClusters.restrict_rootAbsolute_eq line 61
8. lemma OAI.CriticalPercolation.FiniteClusters.eventually_incident_subset line 68
9. lemma OAI.CriticalPercolation.FiniteClusters.measurable_restrict line 81
10. lemma OAI.CriticalPercolation.FiniteClusters.restricted_rootAbsolute_integral line 85
11. lemma OAI.CriticalPercolation.FiniteClusters.ae_finite_clusters line 96
12. theorem OAI.CriticalPercolation.FiniteClusters.subcritical_rootAbsolute_bound line 103