Finite-stage enumerations: limits and fresh entries

An enumeration in finite stages is a sequence A : ℕ → Finset ℕ. The numbers fresh at stage s are those entering in the transition to stage s + 1. When the stages are monotone, a number is fresh at most once: it has a unique entry stage.

Main definitions

• TauCeti.Enumeration.stageLimit: the set enumerated, the union ⋃ s, (A s : Set ℕ) of all stages, so that Mathlib's union and supremum API applies to it.
• TauCeti.Enumeration.fresh: the numbers entering in the transition to stage s + 1.

Main results

• TauCeti.Enumeration.unique_entry_stage: under monotone stages a number is fresh at most once.
• TauCeti.Enumeration.exists_mem_fresh_of_mem_stageLimit: a number of the limit that is not in the first stage is fresh at some stage.
• TauCeti.Enumeration.finite_prefix_stabilizes: under monotone stages, the stages eventually agree with the limit below any bound.
• TauCeti.Enumeration.agrees_of_no_fresh_below: under monotone stages, if nothing below u enters between stages s and t, then A s and A t agree below u.
• TauCeti.Enumeration.limit_agrees_of_no_fresh_below: under monotone stages, if nothing below u enters after stage s, the limit agrees with A s below u.
• TauCeti.Enumeration.stageLimit_comp_of_cofinal: under monotone stages, reindexing by a clock with cofinal range does not change the limit; in particular neither does shifting the stages.

References

• R. I. Soare, Recursively Enumerable Sets and Degrees, Springer, 1987, Chapter VII.1.

def TauCeti.Enumeration.fresh (A : ℕ → Finset ℕ) (s : ℕ) : Finset ℕ

The numbers entering the enumeration A in the transition to stage s + 1.

@[simp]

theorem TauCeti.Enumeration.mem_fresh {A : ℕ → Finset ℕ} {s x : ℕ} : x ∈ fresh A s ↔ x ∈ A (s + 1) ∧ x ∉ A s

Membership in fresh.

theorem TauCeti.Enumeration.unique_entry_stage {A : ℕ → Finset ℕ} (hA : Monotone A) {s t x : ℕ} (hs : x ∈ fresh A s) (ht : x ∈ fresh A t) : s = t

Unique entry stage. Under monotone stages a number is fresh at most once: once entered, it stays.

The limit of an enumeration

def TauCeti.Enumeration.stageLimit (A : ℕ → Finset ℕ) : Set ℕ

The set enumerated by the stages A: the union of all stages.

theorem TauCeti.Enumeration.stageLimit_eq_iUnion (A : ℕ → Finset ℕ) : stageLimit A = ⋃ (s : ℕ), ↑(A s)

The limit is the union of the stages.

@[simp]

theorem TauCeti.Enumeration.mem_stageLimit {A : ℕ → Finset ℕ} {x : ℕ} : x ∈ stageLimit A ↔ ∃ (s : ℕ), x ∈ A s

Membership in the limit is membership at some stage.

theorem TauCeti.Enumeration.subset_stageLimit (A : ℕ → Finset ℕ) (s : ℕ) : ↑(A s) ⊆ stageLimit A

Every stage is contained in the limit.

theorem TauCeti.Enumeration.stageLimit_mono {A B : ℕ → Finset ℕ} (h : ∀ (s : ℕ), A s ⊆ B s) : stageLimit A ⊆ stageLimit B

The limit is monotone in the stages.

theorem TauCeti.Enumeration.mem_stageLimit_of_mem_fresh {A : ℕ → Finset ℕ} {s x : ℕ} (hx : x ∈ fresh A s) : x ∈ stageLimit A

A fresh entry belongs to the limit.

theorem TauCeti.Enumeration.exists_mem_fresh_of_mem_stageLimit {A : ℕ → Finset ℕ} {x : ℕ} (hx : x ∈ stageLimit A) (h0 : x ∉ A 0) : ∃ (s : ℕ), x ∈ fresh A s

An entry stage. A number of the limit that is not in the first stage is fresh at some stage: the stage before the first one containing it.

theorem TauCeti.Enumeration.mem_stageLimit_iff_eventually {A : ℕ → Finset ℕ} (hA : Monotone A) {x : ℕ} : x ∈ stageLimit A ↔ ∃ (s₀ : ℕ), ∀ (s : ℕ), s₀ ≤ s → x ∈ A s

Under monotone stages, a number is in the limit exactly when it is in every late enough stage.

theorem TauCeti.Enumeration.finite_prefix_stabilizes {A : ℕ → Finset ℕ} (hA : Monotone A) (u : ℕ) : ∃ (s₀ : ℕ), ∀ (s : ℕ), s₀ ≤ s → ∀ x < u, x ∈ A s ↔ x ∈ stageLimit A

Finite-prefix stabilization. Under monotone stages, the stages eventually agree with the limit below any bound u.

theorem TauCeti.Enumeration.stageLimit_comp_of_cofinal {A : ℕ → Finset ℕ} (hA : Monotone A) {c : ℕ → ℕ} (hc : ∀ (s : ℕ), ∃ (t : ℕ), s ≤ c t) : stageLimit (A ∘ c) = stageLimit A

Reindexing by a clock with cofinal range. Under monotone stages, reading the stages along a clock c whose range is cofinal, so that every stage is at most some value of c, gives the same limit. The clock need not increase: it may return to small stages infinitely often.

theorem TauCeti.Enumeration.stageLimit_shift {A : ℕ → Finset ℕ} (hA : Monotone A) (k : ℕ) : (stageLimit fun (s : ℕ) => A (s + k)) = stageLimit A

Stage shifts. Under monotone stages, dropping the first k stages does not change the limit.

theorem TauCeti.Enumeration.agrees_of_no_fresh_below {A : ℕ → Finset ℕ} (hA : Monotone A) {s t u : ℕ} (hst : s ≤ t) (h : ∀ (t' : ℕ), s ≤ t' → t' < t → ∀ z < u, z ∉ fresh A t') (z : ℕ) : z < u → (z ∈ A s ↔ z ∈ A t)

No new entries below u between two stages. Under monotone stages, if nothing below u enters from stage s up to a later stage t, then below u the stages A s and A t agree.

theorem TauCeti.Enumeration.limit_agrees_of_no_fresh_below {A : ℕ → Finset ℕ} (hA : Monotone A) {s u : ℕ} (h : ∀ (t : ℕ), s ≤ t → ∀ z < u, z ∉ fresh A t) (z : ℕ) : z < u → (z ∈ A s ↔ z ∈ stageLimit A)

No new entries below u. Under monotone stages, if nothing below u enters after stage s, then below u the limit agrees with A s.