ReturnTowerLevels.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Disjoint towers for positive first return times

def OAI.DukePrimeDegree.firstReturnLevel line 12
Source documentation
The points of S whose first positive return occurs at time n+1.
```
def firstReturnLevel {Y : Type*} (T : Y → Y) (S : Set Y) (n : ℕ) : Set Y :=
…
```
theorem OAI.DukePrimeDegree.measurableSet_firstReturnLevel line 15
theorem OAI.DukePrimeDegree.firstReturnLevel_unique line 28

theorem OAI.DukePrimeDegree.firstReturnTower_unique line 38

Source documentation

Distinct levels and heights cannot meet after translating up their return towers. No recurrence or ergodicity hypothesis is needed.

theorem firstReturnTower_unique {Y : Type*} (T : Y → Y) (hT : Injective T)
    (S : Set Y) {n m j k : ℕ} {x y : Y}
    (hx : x ∈ firstReturnLevel T S n) (hy : y ∈ firstReturnLevel T S m)
    (hj : j ≤ n) (hk : k ≤ m) (he : T^[j] x=T^[k] y) : n=m ∧ j=k := by
…

Mentions: OAI.DukePrimeDegree.firstReturnLevel

def OAI.DukePrimeDegree.firstReturnTower line 60
theorem OAI.DukePrimeDegree.pairwise_disjoint_firstReturnTower line 63