OAI/NumberTheory/DukePrimeDegree/Dynamics/CanonicalSubgroupComponents.lean

Ergodic components over the full subgroup's invariant sigma algebra

The orbit averages come from a countable dense subgroup. Their L² limits extend to the full group and have exactly invariant measurable versions. Consequently the full invariant sigma conditional kernel, the same kernel used by diagonal covariance, has ergodic components.