OAI/Probability/CriticalPercolation/Modular/HeavyDiscrepancy.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalPercolation.ennreal_tendsto_zero_of_uniform_tail line 16
2. lemma OAI.CriticalPercolation.BondGraph.clusterPeakRatio_ne_zero_of_mass_ne_top line 34
3. lemma OAI.CriticalPercolation.BondGraph.normalizedDiscrepancy_le_ratio_add_tail line 42
4. lemma OAI.CriticalPercolation.BondGraph.expected_heavy_normalizedDiscrepancy_bound line 65
5. theorem OAI.CriticalPercolation.BondGraph.tendsto_expected_heavy_normalizedDiscrepancy line 96