SeparatedOrbitCover.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Countable separated covers for the diagonal-map section construction

def OAI.DukePrimeDegree.finiteOrbitNeighbor line 18
lemma OAI.DukePrimeDegree.finiteOrbitNeighbor_symm line 21
def OAI.DukePrimeDegree.homeomorphOrbitSetoid line 31
Source documentation
The orbit relation is used only to say that the section meets each orbit. Its finite-neighbor relation controls the measure of the section.
```
def homeomorphOrbitSetoid (e : Y ≃ₜ Y) : Setoid Y where
…
```
lemma OAI.DukePrimeDegree.finiteOrbitNeighbor_orbit line 45
lemma OAI.DukePrimeDegree.exists_open_finite_orbit_separated line 53
lemma OAI.DukePrimeDegree.measurableSet_finiteOrbitNeighbor line 81

theorem OAI.DukePrimeDegree.exists_countable_finite_orbit_cover line 105

Source documentation

A countable separated cover exists inside any measurable set with no short periodic points. The set need not be invariant or ergodic.

theorem exists_countable_finite_orbit_cover (e : Y ≃ₜ Y) (N : ℕ)
    {A : Set Y} (hA : MeasurableSet A)
    (hfree : ∀ x ∈ A, ∀ k : Fin N, (e^(k.val+1)) x ≠ x) :
    ∃ C : ℕ → Set Y, (∀ n, MeasurableSet (C n)) ∧ (⋃ n, C n)=A ∧
      ∀ n, ∀ x ∈ C n, ∀ y ∈ C n, finiteOrbitNeighbor e N x y → x=y := by
…

Mentions: OAI.DukePrimeDegree.finiteOrbitNeighbor

theorem OAI.DukePrimeDegree.exists_finite_orbit_section line 136

Source documentation

A measurable separated section meets every orbit represented in A.

theorem exists_finite_orbit_section (e : Y ≃ₜ Y) (N : ℕ)
    {A : Set Y} (hA : MeasurableSet A)
    (hfree : ∀ x ∈ A, ∀ k : Fin N, (e^(k.val+1)) x ≠ x) :
    ∃ S : Set Y, MeasurableSet S ∧ S ⊆ A ∧
      (∀ x ∈ S, ∀ y ∈ S, finiteOrbitNeighbor e N x y → x=y) ∧
      ∀ x ∈ A, ∃ y ∈ S, (homeomorphOrbitSetoid e).r x y := by
…

Mentions: OAI.DukePrimeDegree.finiteOrbitNeighbor, OAI.DukePrimeDegree.homeomorphOrbitSetoid