OAI/NumberTheory/DukePrimeDegree/Dynamics/LatticeInvariantVersions.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Exact invariant versions for a matrix subgroup

The subgroup itself need not be closed. Its closure preserves the measure and fixes the same L² vectors. Haar averaging on that closed subgroup produces a version measurable for the original subgroup's exact invariant sigma algebra.

  1. theorem OAI.DukePrimeDegree.lattice_pointwise_invariant_version line 24