OAI/Probability/UnimodularPercolation/Transport/InvariantRoot.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Haar measures and root transport for the full automorphism group.

  1. instance OAI.Percolation.fullGraphAutMeasurableSpace line 19
  2. instance OAI.Percolation.graphAutBorel line 22
  3. def OAI.Percolation.graphAutHaar line 24
  4. instance OAI.Percolation.graphAutHaar_isHaar line 29
  5. theorem OAI.Percolation.graphStabilizer_eq_action line 36
  6. theorem OAI.Percolation.graphStabilizer_inv line 40
  7. theorem OAI.Percolation.graphAutHaar_stabilizer_pos line 46
  8. theorem OAI.Percolation.graphAutHaar_stabilizer_finite line 53
  9. def OAI.Percolation.GraphUnimodular line 58
  10. theorem OAI.Percolation.graphAutHaar_invInvariant line 62
  11. theorem OAI.Percolation.exists_rootTransport_of_unimodular line 82