SingleBlockErgodicity.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

An actual ergodic root flow on a single block component

For a fixed coordinate block, the group generated by its root groups has the same invariant measurable sets as any one of its nontrivial root flows. The Mautner argument proves this for the actual lattice action. The coordinate block is not required to be the whole ambient space.

def OAI.DukePrimeDegree.singleBlockRootGroup line 22
lemma OAI.DukePrimeDegree.root_mem_singleBlockRootGroup line 26
lemma OAI.DukePrimeDegree.singleBlockRootGroup_le_of_roots line 31
theorem OAI.DukePrimeDegree.diagonal_normalizes_singleBlockRootGroup line 43
Source documentation
The same block component can be transported by the actual diagonal action. This concerns covariance of components, not invariance of each individual component.
```
theorem diagonal_normalizes_singleBlockRootGroup {n : ℕ}
    (S : Set (Fin n)) (ell : Fin n → ℝ) (hell : ∑ i, ell i = 0) (t : ℝ) :
    diagonalOneParameter ell hell t ∈
      Subgroup.normalizer (singleBlockRootGroup S : Set (G n)) := by
…
```
Mentions: OAI.DukePrimeDegree.singleBlockRootGroup
theorem OAI.DukePrimeDegree.root_ergodic_of_single_block_ergodic line 67
Source documentation
The one-parameter subgroup used for generic points is ergodic on a genuine single-block ergodic component. No diagonal-ergodicity input is used, and other blocks need not act ergodically on that component.
```
theorem root_ergodic_of_single_block_ergodic {n : ℕ}
    (S : Set (Fin n)) {i j : Fin n} (hij : i ≠ j) (hi : i ∈ S) (hj : j ∈ S)
    (μ : Measure (X n)) [IsFiniteMeasure μ]
    [ErgodicSMul (singleBlockRootGroup S) (X n) μ] :
    let := rootTranslationAction hij
…
```
Mentions: OAI.DukePrimeDegree.singleBlockRootGroup, OAI.DukePrimeDegree.rootTranslationAction
theorem OAI.DukePrimeDegree.single_block_root_ergodic_decomposition line 133
Source documentation
The required root-generic components follow from the proved lattice ergodic decomposition, rather than a separately assumed component law.
```
theorem single_block_root_ergodic_decomposition {n : ℕ}
    (S : Set (Fin n)) {i j : Fin n} (hij : i ≠ j) (hi : i ∈ S) (hj : j ∈ S)
    (μ : Measure (X n)) [IsProbabilityMeasure μ]
    (hH : singleBlockRootGroup S ≤ invariantRightSubgroup μ) :
    let := rootTranslationAction hij
…
```
Mentions: OAI.DukePrimeDegree.singleBlockRootGroup, OAI.DukePrimeDegree.rootTranslationAction