OAI/Probability/CriticalPercolation/Criticality/MainResidualBoundary.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.BondGraph.twoHeavyDistinctEvent line 18
2. lemma OAI.CriticalPercolation.BondGraph.measurableSet_twoHeavyDistinctEvent line 22
3. lemma OAI.CriticalPercolation.BondGraph.atMostOneInfinite_ae_of_no_light_or_two_heavy line 27
4. lemma OAI.CriticalPercolation.BondGraph.positive_light_or_two_heavy_of_exponential_critical_percolation line 54
5. theorem OAI.CriticalPercolation.BondGraph.main_residual_boundary line 72