OAI/Probability/CriticalPercolation/Criticality/TwoPoint.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.Sharpness.twoPoint line 16
2. lemma OAI.CriticalPercolation.Sharpness.hit_singleton_eq line 18
3. lemma OAI.CriticalPercolation.Sharpness.twoPoint_nonneg line 23
4. lemma OAI.CriticalPercolation.Sharpness.finite_contraction line 25
5. lemma OAI.CriticalPercolation.Sharpness.finite_probability_connection line 49
6. theorem OAI.CriticalPercolation.Sharpness.subcritical_susceptibility line 60
7. theorem OAI.CriticalPercolation.Sharpness.summable_subcritical_twoPoint line 86