OAI/Probability/CriticalPercolation/Modular/DiscrepancyTail.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalPercolation.ennreal_geometric_band line 15
2. lemma OAI.CriticalPercolation.BondGraph.normalizedClusterVolume_ne_top line 33
3. def OAI.CriticalPercolation.BondGraph.discrepancyVolumeTail line 39
4. lemma OAI.CriticalPercolation.BondGraph.measurable_discrepancyVolumeTail line 42
5. lemma OAI.CriticalPercolation.BondGraph.discrepancyVolumeTail_le_bands line 48
6. lemma OAI.CriticalPercolation.BondGraph.expected_discrepancyTail_bound line 63