OAI/Probability/CriticalPercolation/Modular/GraphModular.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CriticalPercolation.BondGraph.stabilizerOrbit line 16
  2. lemma OAI.CriticalPercolation.BondGraph.mem_stabilizerOrbit line 19
  3. lemma OAI.CriticalPercolation.BondGraph.self_mem_stabilizerOrbit line 28
  4. lemma OAI.CriticalPercolation.BondGraph.stabilizerOrbit_finite line 31
  5. def OAI.CriticalPercolation.BondGraph.suborbitCard line 40
  6. lemma OAI.CriticalPercolation.BondGraph.suborbitCard_pos line 42
  7. lemma OAI.CriticalPercolation.BondGraph.suborbitCard_eq_relIndex line 46
  8. lemma OAI.CriticalPercolation.BondGraph.Aut.stabilizerOrbit_image line 55
  9. lemma OAI.CriticalPercolation.BondGraph.Aut.suborbitCard line 77
  10. def OAI.CriticalPercolation.BondGraph.modularRatio line 83
  11. lemma OAI.CriticalPercolation.BondGraph.modularRatio_eq_relativeMass line 85
  12. lemma OAI.CriticalPercolation.BondGraph.modularRatio_pos line 89
  13. lemma OAI.CriticalPercolation.BondGraph.modularRatio_cocycle line 94
  14. lemma OAI.CriticalPercolation.BondGraph.modularRatio_self line 102
  15. lemma OAI.CriticalPercolation.BondGraph.Aut.modularRatio line 105
  16. def OAI.CriticalPercolation.BondGraph.CombinatoriallyUnimodular line 109
  17. lemma OAI.CriticalPercolation.BondGraph.CombinatoriallyUnimodular.modularRatio line 112
  18. lemma OAI.CriticalPercolation.BondGraph.CombinatoriallyUnimodular.rootWeight_invariant line 119
  19. lemma OAI.CriticalPercolation.BondGraph.modularRatio_card_balance line 125