OAI/NumberTheory/DukePrimeDegree/Dynamics/MautnerLatticeL2.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Mautner for the actual lattice L² action

Only the specified subgroup preserves the measure. Pullback by its right action is a continuous isometric action on L². Thus a root-flow invariant L² observable is also invariant under the opposite root and the associated diagonal elements of that subgroup.

  1. def OAI.DukePrimeDegree.inverseDomainHom line 23
  2. lemma OAI.DukePrimeDegree.continuous_inverseDomainHom line 28
  3. theorem OAI.DukePrimeDegree.ae_opposite_root_fixed_of_L2_root_fixed line 32
  4. theorem OAI.DukePrimeDegree.ae_root_pair_diagonal_fixed_of_L2_root_fixed line 64