OAI/Probability/CriticalPercolation/Modular/ClusterMassEndpointFinite.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalPercolation.FiniteClusters.clusterTail_iff_size line 18
2. lemma OAI.CriticalPercolation.FiniteClusters.size_insert_disconnected line 26
3. lemma OAI.CriticalPercolation.FiniteClusters.size_insert_connected line 34
4. lemma OAI.CriticalPercolation.FiniteClusters.edgeMass_gap line 40
5. lemma OAI.CriticalPercolation.FiniteClusters.finite_expect_edgeDiscrepancy line 58
6. lemma OAI.CriticalPercolation.FiniteClusters.finite_endpoint_le_expect line 90
7. lemma OAI.CriticalPercolation.FiniteClusters.finite_endpoint_le_integral line 109