OAI/Probability/CriticalPercolation/Modular/ModularIncidence.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalPercolation.BondGraph.bondWeight line 14
2. lemma OAI.CriticalPercolation.BondGraph.bondWeight_ne_top line 16
3. lemma OAI.CriticalPercolation.BondGraph.bondWeight_change_base line 21
4. lemma OAI.CriticalPercolation.BondGraph.Aut.bondWeight line 29
5. lemma OAI.CriticalPercolation.BondGraph.incidence_stabilizerOrbit_subset_ball line 40
6. lemma OAI.CriticalPercolation.BondGraph.stabilizerWeight_le_ball_bound line 47
7. lemma OAI.CriticalPercolation.BondGraph.common_bond_ball_one line 61
8. lemma OAI.CriticalPercolation.BondGraph.bondWeight_le_at_end line 72
9. lemma OAI.CriticalPercolation.BondGraph.weighted_incidence_le line 93