CountableOrbitSection.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A measurable section from a countable separated cover

The finite-neighbor relation in the application consists of the first few forward and backward iterates. Removing earlier neighbors leaves a separated section meeting every orbit in the cover. This construction requires no ergodicity of the selected diagonal map.

theorem OAI.DukePrimeDegree.exists_measurable_orbit_section line 19

Source documentation

The elementary marker construction, with orbit equivalence separated from the finite-neighbor relation.

theorem exists_measurable_orbit_section
    {Y : Type*} [MeasurableSpace Y] (E : Setoid Y)
    (R : Y → Y → Prop) (hRsymm : ∀ ⦃x y⦄, R x y → R y x)
    (hRE : ∀ x y, R x y → E.r x y)
    (C : ℕ → Set Y) (hC : ∀ n, MeasurableSet (C n))
    (hRC : ∀ n, MeasurableSet {x | ∃ y ∈ C n, R x y})
    (hsep : ∀ n, ∀ x ∈ C n, ∀ y ∈ C n, R x y → x=y) :
    ∃ S : Set Y, MeasurableSet S ∧ S ⊆ ⋃ n, C n ∧
      (∀ x ∈ S, ∀ y ∈ S, R x y → x=y) ∧
      ∀ x ∈ ⋃ n, C n, ∃ y ∈ S, E.r x y := by
…