OAI/Probability/CriticalPercolation/Modular/NormalizedDiscrepancy.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.BondGraph.normalizedAbsoluteDiscrepancy line 15
2. lemma OAI.CriticalPercolation.BondGraph.measurable_normalizedAbsoluteDiscrepancy line 18
3. lemma OAI.CriticalPercolation.BondGraph.Aut.weightedDiscrepancy line 23
4. lemma OAI.CriticalPercolation.BondGraph.Aut.normalizedAbsoluteDiscrepancy line 43
5. lemma OAI.CriticalPercolation.BondGraph.normalizedAbsoluteDiscrepancy_eq_of_reachable line 49
6. lemma OAI.CriticalPercolation.BondGraph.normalizedAbsoluteDiscrepancy_le line 60
7. def OAI.CriticalPercolation.BondGraph.discrepancyVolumeBand line 72
8. lemma OAI.CriticalPercolation.BondGraph.measurable_discrepancyVolumeBand line 76
9. lemma OAI.CriticalPercolation.BondGraph.band_volume_ratio line 83
10. lemma OAI.CriticalPercolation.BondGraph.band_volume_peak line 98
11. theorem OAI.CriticalPercolation.BondGraph.expected_discrepancyBand_peak line 116