OAI/NumberTheory/DukePrimeDegree/Dynamics/InvariantVersion.lean

A strictly invariant version of an almost-everywhere invariant observable

For a measurable group action, use the essential constant value of the observable along the orbit with respect to a nonzero translation-invariant measure on the acting group. Fubini gives agreement almost everywhere; translation invariance makes the new version invariant at every point. This supplies the pointwise neutral invariance needed for selecting noncentral return pairs.