OAI/Probability/CriticalPercolation/Modular/ModularCharacter.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalPercolation.BondGraph.modularRatio_aut_translate line 14
2. lemma OAI.CriticalPercolation.BondGraph.modularRatio_aut_base line 20
3. def OAI.CriticalPercolation.BondGraph.modularCharacter line 28
4. lemma OAI.CriticalPercolation.BondGraph.modularCharacter_apply line 36
5. lemma OAI.CriticalPercolation.BondGraph.modularCharacter_pos line 40
6. lemma OAI.CriticalPercolation.BondGraph.modularCharacter_base line 44
7. def OAI.CriticalPercolation.BondGraph.modularKernel line 49
8. lemma OAI.CriticalPercolation.BondGraph.mem_modularKernel line 52
9. lemma OAI.CriticalPercolation.BondGraph.stabilizer_le_modularKernel line 62
10. lemma OAI.CriticalPercolation.BondGraph.modularKernel_transitive_on_level line 70
11. def OAI.CriticalPercolation.BondGraph.modularCoordinate line 82
12. lemma OAI.CriticalPercolation.BondGraph.modularCoordinate_val line 86
13. def OAI.CriticalPercolation.BondGraph.modularUnitCharacter line 89
14. lemma OAI.CriticalPercolation.BondGraph.modularCoordinate_equivariant line 95
15. lemma OAI.CriticalPercolation.BondGraph.unit_stabilizer_le_kernel line 101