FiniteFlowGenericSets.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

One generic set for the finite separating observables

The finite family needed to separate the compact set of limiting shears uses one measurable good set and one common time threshold. Only ergodicity of the actual full real-flow component is used.

theorem OAI.DukePrimeDegree.exists_finite_uniform_integer_flow_generic_set line 21
theorem OAI.DukePrimeDegree.exists_finite_uniform_root_flow_generic_set line 55
Source documentation
The common good set applies to an actual ergodic component of a root flow on the arithmetic quotient.
```
theorem exists_finite_uniform_root_flow_generic_set
    {n : ℕ} {i j : Fin n} (hij : i ≠ j) {I : Type*} [Fintype I]
    (ν : Measure (X n)) [IsProbabilityMeasure ν]
    (herg : let := rootTranslationAction hij
…
```
Mentions: OAI.DukePrimeDegree.rootTranslationAction