OAI/Probability/CriticalPercolation/Modular/LightTwoPointDecay.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.BondGraph.upperEscapeEvent line 17
2. lemma OAI.CriticalPercolation.BondGraph.measurableSet_upperEscapeEvent line 20
3. lemma OAI.CriticalPercolation.BondGraph.upperEscapeEvent_antitone line 25
4. lemma OAI.CriticalPercolation.BondGraph.not_iInter_upperEscape_of_mass_finite line 29
5. lemma OAI.CriticalPercolation.BondGraph.tendsto_upperEscape_zero line 37
6. lemma OAI.CriticalPercolation.BondGraph.Aut.upperEscapeEvent_preimage line 53
7. lemma OAI.CriticalPercolation.BondGraph.Aut.upperEscapeEvent_real line 71
8. lemma OAI.CriticalPercolation.BondGraph.uniform_upperEscape_small line 81
9. lemma OAI.CriticalPercolation.BondGraph.stabilizerWeight_ge_one_either line 96
10. lemma OAI.CriticalPercolation.BondGraph.twoPoint_symm line 113
11. theorem OAI.CriticalPercolation.BondGraph.uniform_twoPoint_decay_of_finite_mass line 123
12. theorem OAI.CriticalPercolation.BondGraph.nonunimodular_critical_twoPoint_decay line 146