OAI/Probability/CriticalPercolation/Modular/SignedDiscrepancyContinuity.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.BondGraph.normalizedSignedDiscrepancy line 19
2. lemma OAI.CriticalPercolation.BondGraph.normalizedSignedDiscrepancy_heavy line 22
3. lemma OAI.CriticalPercolation.BondGraph.enorm_normalizedSignedDiscrepancy line 26
4. lemma OAI.CriticalPercolation.BondGraph.measurable_normalizedSignedDiscrepancy line 36
5. lemma OAI.CriticalPercolation.BondGraph.norm_normalizedSignedDiscrepancy_le line 40
6. lemma OAI.CriticalPercolation.BondGraph.eventually_incident_of_exhaustion line 48
7. lemma OAI.CriticalPercolation.BondGraph.eventually_mem_of_exhaustion line 63
8. lemma OAI.CriticalPercolation.BondGraph.tendsto_weightedDiscrepancy_of_exhaustion line 73
9. lemma OAI.CriticalPercolation.BondGraph.tendsto_modularMass_toReal_of_exhaustion line 109
10. lemma OAI.CriticalPercolation.BondGraph.tendsto_normalizedSignedDiscrepancy_finiteMass line 136
11. lemma OAI.CriticalPercolation.BondGraph.integrable_normalizedSignedDiscrepancy line 149
12. theorem OAI.CriticalPercolation.BondGraph.tendsto_L1_normalizedSignedDiscrepancy line 159
13. theorem OAI.CriticalPercolation.BondGraph.tendsto_expected_normalizedSignedDiscrepancy line 217