OAI/Probability/UnimodularPercolation/Graph/Automorphisms.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Locally compact graph automorphism groups and unimodular root data.

  1. def OAI.Percolation.graphAut line 20
  2. theorem OAI.Percolation.mem_vertexAut_iff line 32
  3. abbrev OAI.Percolation.graphOrbitType line 56
  4. instance OAI.Percolation.graphOrbitType_nonempty line 58
  5. def OAI.Percolation.graphOrbitRoot line 61
  6. theorem OAI.Percolation.graphOrbitRoot_cover line 63
  7. theorem OAI.Percolation.graphOrbitRoot_separate line 71
  8. theorem OAI.Percolation.finite_graphOrbitType line 78
  9. theorem OAI.Percolation.isClosed_vertexAut line 97
  10. theorem OAI.Percolation.isCompact_vertexStabilizer line 108
  11. theorem OAI.Percolation.graphAut_continuous_apply line 128
  12. theorem OAI.Percolation.graphAut_isOpen_stabilizer line 132
  13. theorem OAI.Percolation.graphAut_isCompact_stabilizer line 136
  14. theorem OAI.Percolation.graphAut_locallyCompact line 150
  15. instance OAI.Percolation.graphAutSecondCountable line 170
  16. instance OAI.Percolation.graphAutMeasurableSpace line 174
  17. instance OAI.Percolation.graphAutBorelSpace line 177
  18. def OAI.Percolation.graphHaar line 180
  19. theorem OAI.Percolation.graphHaar_isHaar line 186
  20. theorem OAI.Percolation.graphHaar_regular line 192
  21. theorem OAI.Percolation.graphStabilizer_volume_pos line 199
  22. theorem OAI.Percolation.graphHaar_rootTransport line 212
  23. theorem OAI.Percolation.exists_graphHaar_rootData line 228
  24. theorem OAI.Percolation.exists_rootData_of_unimodular line 251