OAI/NumberTheory/DukePrimeDegree/Dynamics/AlmostInvariantComponents.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Conditional component invariance from almost invariant base sets

Pointwise invariance of every set in the conditioning sigma algebra is stronger than needed. Almost invariance with respect to the ambient probability already makes the conditional component measures invariant. This permits Mautner's L² argument to act on the full-subgroup components without asserting that the new map normalizes the subgroup.

  1. theorem OAI.DukePrimeDegree.condExpKernel_invariant_of_ae_invariant_sets line 22