RootPairErgodicity.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Ergodicity of a root inside its actual two-root group

The chosen root is ergodic on an ergodic component of the group generated by it and its opposite. This follows from the concrete Mautner argument, not from an implication from diagonal ergodicity. Only the two-root group is required to preserve the measure.

def OAI.DukePrimeDegree.oppositeRootPairGroup line 22
lemma OAI.DukePrimeDegree.root_mem_oppositeRootPairGroup line 26
lemma OAI.DukePrimeDegree.opposite_root_mem_oppositeRootPairGroup line 30
lemma OAI.DukePrimeDegree.subgroup_le_invariantRightSubgroup_of_invariant_action line 35
theorem OAI.DukePrimeDegree.root_ergodic_of_opposite_root_pair_ergodic line 44
theorem OAI.DukePrimeDegree.opposite_root_pair_ergodic_decomposition line 124
Source documentation
The existing measurable decomposition can be taken over the actual two-root group. Each resulting component is then ergodic for the full root flow as well. No invariance under the rest of the diagonal group is asserted for these components.
```
theorem opposite_root_pair_ergodic_decomposition {n : ℕ} {i j : Fin n}
    (hij : i ≠ j) (μ : Measure (X n)) [IsProbabilityMeasure μ]
    (hH : oppositeRootPairGroup hij ≤ invariantRightSubgroup μ) :
    let := rootTranslationAction hij
…
```
Mentions: OAI.DukePrimeDegree.oppositeRootPairGroup, OAI.DukePrimeDegree.rootTranslationAction