OAI/NumberTheory/DukePrimeDegree/Dynamics/MautnerBlockL2.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The one-block Mautner argument on actual lattice observables

A root-invariant square-integrable observable is invariant under every root of the same coordinate block, provided those roots preserve the measure. The group used in the proof is the specified subgroup, not the full special linear group.

  1. theorem OAI.DukePrimeDegree.ae_block_root_fixed_of_L2_root_fixed line 22