RootFlowGeneric.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Generic sets for the actual root flow

The action used here is the actual right transvection action on the integer-lattice quotient. Its invariant probability has an ergodic decomposition for the entire real flow. On each such ergodic component, the uniform generic-set theorem uses no chosen-time ergodicity premise. The further homogeneous-support conclusion is not asserted here.

theorem OAI.DukePrimeDegree.root_flow_ergodic_decomposition line 24
theorem OAI.DukePrimeDegree.exists_uniform_root_flow_generic_set line 40
Source documentation
Uniform generic sets on an actual root-flow ergodic component.
```
theorem exists_uniform_root_flow_generic_set {n : ℕ} {i j : Fin n} (hij : i ≠ j)
    (ν : Measure (X n)) [IsProbabilityMeasure ν]
    (herg : let := rootTranslationAction hij
…
```
Mentions: OAI.DukePrimeDegree.rootTranslationAction