OAI/Probability/UnimodularPercolation/Transport/Haar.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Haar-measure transport for graph automorphism actions.

  1. theorem OAI.Percolation.haar_invInvariant_of_rightInvariant line 18
  2. def OAI.Percolation.actionStabilizer line 51
  3. def OAI.Percolation.actionOrbit line 54
  4. theorem OAI.Percolation.actionOrbit_self line 58
  5. theorem OAI.Percolation.actionOrbit_eq_of_mem line 62
  6. theorem OAI.Percolation.orbit_fiber_measure line 75
  7. theorem OAI.Percolation.orbit_map_measure line 96
  8. theorem OAI.Percolation.integral_orbit_sum line 111
  9. theorem OAI.Percolation.orbit_mass_balance line 127
  10. def OAI.Percolation.inverseStabilizerWeight line 146
  11. theorem OAI.Percolation.inverseStabilizerWeight_pos line 152
  12. theorem OAI.Percolation.inverseStabilizerWeight_sum line 160
  13. theorem OAI.Percolation.tsum_eq_sum_orbits line 171
  14. theorem OAI.Percolation.rootTransport_of_invariant_measure line 196