OAI/Probability/CriticalPercolation/Modular/HeavyHarris.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.BondGraph.massTailEvent line 15
2. lemma OAI.CriticalPercolation.BondGraph.massTailEvent_upper line 18
3. lemma OAI.CriticalPercolation.BondGraph.massTailEvent_finiteWitness line 21
4. lemma OAI.CriticalPercolation.BondGraph.measurableSet_massTailEvent line 38
5. lemma OAI.CriticalPercolation.BondGraph.heavyClusterEvent_eq_iInter_massTail line 42
6. lemma OAI.CriticalPercolation.BondGraph.massTailEvent_antitone line 58
7. lemma OAI.CriticalPercolation.BondGraph.tendsto_real_massTail line 62
8. lemma OAI.CriticalPercolation.BondGraph.harris_heavyClusterEvent line 71