OAI/Probability/UnimodularPercolation/Cayley/Geometry.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Cayley graphs, translation symmetries and root transport.

  1. def OAI.Percolation.AmenableGroup line 17

    Also declared: ComparatorChallenges/CayleyPercolation.lean:57 (same declaration text).

  2. def OAI.Percolation.CayleyEdge line 22

    Also declared: ComparatorChallenges/CayleyPercolation.lean:62 (same declaration text).

  3. def OAI.Percolation.cayleyGraph line 25

    Also declared: ComparatorChallenges/CayleyPercolation.lean:65 (same declaration text).

  4. lemma OAI.Percolation.amenableGroup_of_finite line 32
  5. lemma OAI.Percolation.infinite_of_nonamenable line 43
  6. lemma OAI.Percolation.cayleyGraph_injective line 48
  7. lemma OAI.Percolation.cayley_adj_of_mem line 51
  8. lemma OAI.Percolation.cayley_adj_iff line 55
  9. lemma OAI.Percolation.cayley_loopless line 68
  10. lemma OAI.Percolation.cayley_locallyFinite line 75
  11. def OAI.Percolation.cayleyEdgeTranslation line 92
  12. lemma OAI.Percolation.cayley_translation_isAut line 106
  13. lemma OAI.Percolation.cayley_translation_mem line 111
  14. lemma OAI.Percolation.cayley_quasiTransitive line 115
  15. lemma OAI.Percolation.cayley_connected line 121
  16. lemma OAI.Percolation.cayley_rootTransport line 141