OAI/Probability/UnimodularPercolation/Cayley/Folner.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The group Følner criterion and nonamenable Cayley graphs.

  1. def OAI.Percolation.rightTranslate line 18
  2. lemma OAI.Percolation.card_rightTranslate line 21
  3. lemma OAI.Percolation.rightTranslate_one line 25
  4. lemma OAI.Percolation.rightTranslate_mul line 28
  5. lemma OAI.Percolation.rightTranslate_sdiff line 32
  6. def OAI.Percolation.rightDefect line 36
  7. lemma OAI.Percolation.card_sdiff_triangle line 40
  8. lemma OAI.Percolation.rightDefect_mul_le line 48
  9. lemma OAI.Percolation.rightDefect_inv line 58
  10. lemma OAI.Percolation.rightDefect_le_boundary line 67
  11. lemma OAI.Percolation.cayley_hV_pos line 95