OAI/NumberTheory/DukePrimeDegree/Dynamics/DenseInvariantFunctions.lean

Almost invariance extends from a dense subgroup

Continuity of the actual pullback representation on lattice L² extends almost invariance of an observable from a dense subgroup. This does not turn pointwise invariance into a topological assertion about a measurable observable; the continuous object is its L² equivalence class.