OAI/Probability/CriticalPercolation/Modular/CriticalHeavyNull.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalPercolation.BondGraph.Aut.heavyClusterEvent_iff line 20
2. lemma OAI.CriticalPercolation.BondGraph.Aut.heavyClusterEvent_measure line 27
3. lemma OAI.CriticalPercolation.BondGraph.heavyClusterEvent_pos_all line 38
4. lemma OAI.CriticalPercolation.BondGraph.uniform_heavy_probability line 59
5. lemma OAI.CriticalPercolation.BondGraph.uniqueHeavy_twoPoint_lower line 77
6. theorem OAI.CriticalPercolation.BondGraph.exponential_critical_heavy_null line 90
7. theorem OAI.CriticalPercolation.BondGraph.nonunimodular_critical_mass_finite_ae line 117