OAI/Probability/CriticalPercolation/Criticality/LocalDescendingBlock.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.BondGraph.localDescendingFanEvent line 18
2. lemma OAI.CriticalPercolation.BondGraph.localDescendingFanEvent_upper line 21
3. lemma OAI.CriticalPercolation.BondGraph.measurableSet_localDescendingFanEvent line 26
4. lemma OAI.CriticalPercolation.BondGraph.tendsto_localDescendingFan line 32
5. lemma OAI.CriticalPercolation.BondGraph.Aut.localDescendingFanEvent_preimage line 43
6. lemma OAI.CriticalPercolation.BondGraph.Aut.localDescendingFanEvent_real line 56
7. lemma OAI.CriticalPercolation.BondGraph.localDescendingFan_uniform_radius line 66
8. def OAI.CriticalPercolation.BondGraph.separatedDescendingBlockEvent line 80
9. lemma OAI.CriticalPercolation.BondGraph.separatedDescendingBlockEvent_upper line 86
10. lemma OAI.CriticalPercolation.BondGraph.separatedDescendingBlockEvent_finiteWitness line 93
11. lemma OAI.CriticalPercolation.BondGraph.measurableSet_separatedDescendingBlockEvent line 106
12. lemma OAI.CriticalPercolation.BondGraph.localDescendingFan_subset_separatedBlock line 113
13. theorem OAI.CriticalPercolation.BondGraph.counterexample_separated_downward_blocks line 131