OAI/Probability/CriticalPercolation/Modular/WeightedDiscrepancy.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.BondGraph.centeredCoefficient line 16
2. def OAI.CriticalPercolation.BondGraph.weightedIncidenceTerm line 18
3. def OAI.CriticalPercolation.BondGraph.weightedDiscrepancy line 22
4. lemma OAI.CriticalPercolation.BondGraph.abs_centeredCoefficient_le_one line 25
5. lemma OAI.CriticalPercolation.BondGraph.norm_weightedIncidenceTerm_le line 30
6. lemma OAI.CriticalPercolation.BondGraph.summable_weightedIncidence_bound line 39
7. lemma OAI.CriticalPercolation.BondGraph.summable_weightedIncidenceTerm line 48
8. lemma OAI.CriticalPercolation.BondGraph.abs_weightedDiscrepancy_le line 56
9. lemma OAI.CriticalPercolation.BondGraph.measurable_weightedDiscrepancy line 76
10. lemma OAI.CriticalPercolation.BondGraph.weightedIncidenceTerm_change_base line 86
11. lemma OAI.CriticalPercolation.BondGraph.weightedDiscrepancy_change_base line 94