Word cylinders and coordinate flips in Cantor space

A word is a finite list w : List α, read left to right. The point prependWord w x of ℕ → α starts with the letters of w and continues with x, and the word cylinder wordCylinder w is the set of points that start with w, the range of prependWord w. These are the basic open sets of Cantor space ℕ → Bool and of Baire space ℕ → ℕ indexed by the word they begin with. Constructions on Cantor space indexed by words, such as the graphs G_S of Kechris, Solecki and Todorcevic, whose edges join prependWord (s ++ [false]) x and prependWord (s ++ [true]) x, are phrased in this language.

Mathlib's cylinders PiNat.cylinder x n are indexed instead by a point and a length, and PiNat.res x n lists the first n values of x newest first. The two conventions are related by PiNat.wordCylinder_reverse_res, which says that wordCylinder (res x n).reverse is cylinder x n. The point prependWord w x is Mathlib's Stream'.appendStream' w x, and its basic API is derived from Mathlib's lemmas about Stream'.appendStream'. It is typed as a point of ℕ → α because the type synonym Stream' α carries no topology or measurable structure, and Mathlib's lemmas, phrased through Stream'.get, do not apply to evaluation y n by simp or rw.

The coordinate flip PiNat.flipAt n negates the n-th coordinate of a point of Cantor space. It is an involutive homeomorphism, and it maps the cylinder of a word w onto the cylinder of the word obtained by negating the n-th letter of w (PiNat.image_flipAt_wordCylinder). In particular it exchanges the two halves wordCylinder (s ++ [false]) and wordCylinder (s ++ [true]) of wordCylinder s when s has length n: this is the symmetry used in Miller's proof that the graphs G_S have no countable Baire-measurable coloring, and in the proof that eventual equality E₀ is generically ergodic.

Main definitions

• PiNat.prependWord w x: the point that starts with the word w and continues with x.
• PiNat.wordCylinder w: the set of points that start with w.
• PiNat.flipAt n: the homeomorphism of ℕ → Bool negating the n-th coordinate.

Main results

• PiNat.mem_wordCylinder_iff: a point lies in wordCylinder w iff it agrees with w on the first w.length coordinates.
• PiNat.wordCylinder_subset_wordCylinder_iff: over a nontrivial alphabet, inclusion of word cylinders is the reverse of the prefix order on words.
• PiNat.disjoint_wordCylinder_iff: two word cylinders are disjoint iff neither word is a prefix of the other.
• PiNat.isOpenEmbedding_prependWord: over a discrete alphabet, prependWord w is an open embedding onto the clopen set wordCylinder w.
• PiNat.wordCylinder_reverse_res: wordCylinder (res x n).reverse = cylinder x n.
• PiNat.image_flipAt_wordCylinder: flipAt n maps wordCylinder w onto the cylinder of w with its n-th letter negated.

References

• A. S. Kechris, Classical Descriptive Set Theory, Springer-Verlag, 1995, Section 2.D, for cylinders indexed by finite sequences in ℕ → α.
• B. D. Miller, "The graph-theoretic approach to descriptive set theory", Bulletin of Symbolic Logic 18 (2012), 554–575, for the graphs G_S and the coordinate flip.

Prepending a word

def PiNat.prependWord {α : Type u_1} (w : List α) (x : ℕ → α) : ℕ → α

prependWord w x is the point of ℕ → α that starts with the letters of the word w, read left to right, and continues with the point x: Mathlib's Stream'.appendStream' w x, typed as a point of ℕ → α.

theorem PiNat.prependWord_apply_of_lt {α : Type u_1} {w : List α} {x : ℕ → α} {n : ℕ} (h : n < w.length) : prependWord w x n = w[n]

Below w.length, the coordinates of prependWord w x are the letters of w.

@[simp]

theorem PiNat.prependWord_apply_length_add {α : Type u_1} (w : List α) (x : ℕ → α) (n : ℕ) : prependWord w x (w.length + n) = x n

theorem PiNat.prependWord_apply_of_le {α : Type u_1} {w : List α} {x : ℕ → α} {n : ℕ} (h : w.length ≤ n) : prependWord w x n = x (n - w.length)

From w.length on, the coordinates of prependWord w x are those of x, shifted by w.length.

@[simp]

theorem PiNat.prependWord_apply_length {α : Type u_1} (w : List α) (x : ℕ → α) : prependWord w x w.length = x 0

@[simp]

theorem PiNat.prependWord_nil {α : Type u_1} (x : ℕ → α) : prependWord [] x = x

@[simp]

theorem PiNat.prependWord_append {α : Type u_1} (v w : List α) (x : ℕ → α) : prependWord (v ++ w) x = prependWord v (prependWord w x)

Prepending v ++ w is prepending w and then v.

theorem PiNat.prependWord_eq_self {α : Type u_1} {w : List α} {y : ℕ → α} (hy : ∀ (i : ℕ) (h : i < w.length), y i = w[i]) : (prependWord w fun (n : ℕ) => y (w.length + n)) = y

A point is recovered from its first w.length coordinates, here given by the word w, and its remaining coordinates.

theorem PiNat.prependWord_injective {α : Type u_1} (w : List α) : Function.Injective (prependWord w)

Prepending a fixed word is injective.

@[simp]

theorem PiNat.prependWord_inj {α : Type u_1} {w : List α} {x y : ℕ → α} : prependWord w x = prependWord w y ↔ x = y

theorem PiNat.continuous_prependWord {α : Type u_1} [TopologicalSpace α] (w : List α) : Continuous (prependWord w)

For any topology on the alphabet, prepending a word is continuous for the product topology on ℕ → α.

theorem PiNat.measurable_prependWord {α : Type u_1} [MeasurableSpace α] (w : List α) : Measurable (prependWord w)

For any measurable structure on the alphabet, prepending a word is measurable for the product σ-algebra on ℕ → α.

Word cylinders

def PiNat.wordCylinder {α : Type u_1} (w : List α) : Set (ℕ → α)

The cylinder of the word w: the set of points of ℕ → α that start with the letters of w, as the range of prependWord w.

@[simp]

theorem PiNat.range_prependWord {α : Type u_1} (w : List α) : Set.range (prependWord w) = wordCylinder w

@[simp]

theorem PiNat.prependWord_mem_wordCylinder {α : Type u_1} (w : List α) (x : ℕ → α) : prependWord w x ∈ wordCylinder w

theorem PiNat.mem_wordCylinder_iff {α : Type u_1} {w : List α} {y : ℕ → α} : y ∈ wordCylinder w ↔ ∀ (i : ℕ) (h : i < w.length), y i = w[i]

A point lies in the cylinder of w iff its first w.length coordinates are the letters of w, in order.

@[simp]

theorem PiNat.wordCylinder_nil {α : Type u_1} : wordCylinder [] = Set.univ

theorem PiNat.wordCylinder_nonempty {α : Type u_1} [Nonempty α] (w : List α) : (wordCylinder w).Nonempty

Over a nonempty alphabet, every word cylinder is nonempty.

theorem List.IsPrefix.wordCylinder_subset {α : Type u_1} {w v : List α} (h : v <+: w) : PiNat.wordCylinder w ⊆ PiNat.wordCylinder v

A longer word has a smaller cylinder.

theorem PiNat.prefix_or_prefix_of_mem_wordCylinder {α : Type u_1} {w v : List α} {y : ℕ → α} (hv : y ∈ wordCylinder v) (hw : y ∈ wordCylinder w) : v <+: w ∨ w <+: v

If y starts with both words v and w, then one of them is a prefix of the other.

theorem PiNat.wordCylinder_subset_wordCylinder_iff {α : Type u_1} {w v : List α} [Nontrivial α] : wordCylinder w ⊆ wordCylinder v ↔ v <+: w

Over a nontrivial alphabet, inclusion of word cylinders is the reverse of the prefix order on words.

theorem PiNat.disjoint_wordCylinder_iff {α : Type u_1} {w v : List α} [Nonempty α] : Disjoint (wordCylinder v) (wordCylinder w) ↔ ¬(v <+: w ∨ w <+: v)

Two word cylinders are disjoint iff neither word is a prefix of the other.

theorem PiNat.iUnion_wordCylinder_append_singleton {α : Type u_1} (w : List α) : ⋃ (a : α), wordCylinder (w ++ [a]) = wordCylinder w

The cylinder of w is the union of the cylinders of its one-letter extensions.

theorem PiNat.cylinder_eq_wordCylinder {α : Type u_1} {w : List α} {y : ℕ → α} (hy : y ∈ wordCylinder w) : cylinder y w.length = wordCylinder w

The points that start with w are those of the Mathlib cylinder of length w.length around any one of them.

@[simp]

theorem PiNat.cylinder_prependWord_length {α : Type u_1} (w : List α) (x : ℕ → α) : cylinder (prependWord w x) w.length = wordCylinder w

theorem PiNat.reverse_res {α : Type u_1} (x : ℕ → α) (n : ℕ) : (res x n).reverse = List.ofFn fun (i : Fin n) => x ↑i

Mathlib's res x n lists the first n coordinates of x newest first, so its reverse is the word of the first n coordinates of x, read left to right.

@[simp]

theorem PiNat.wordCylinder_reverse_res {α : Type u_1} (x : ℕ → α) (n : ℕ) : wordCylinder (res x n).reverse = cylinder x n

The cylinder of the first n letters of x, read left to right, is Mathlib's cylinder of length n around x.

@[simp]

theorem PiNat.res_prependWord_length_add {α : Type u_1} (w : List α) (x : ℕ → α) (n : ℕ) : res (prependWord w x) (w.length + n) = res x n ++ w.reverse

The first w.length + n coordinates of prependWord w x, newest first, are the first n coordinates of x, newest first, followed by the reversed word w.

theorem PiNat.wordCylinder_eq_iInter {α : Type u_1} (w : List α) : wordCylinder w = ⋂ (i : ℕ), ⋂ (h : i < w.length), (fun (y : ℕ → α) => y i) ⁻¹' {w[i]}

The cylinder of w as the intersection of the coordinate conditions it imposes.

theorem PiNat.isClosed_wordCylinder {α : Type u_1} [TopologicalSpace α] [T1Space α] (w : List α) : IsClosed (wordCylinder w)

Over a T₁ alphabet, every word cylinder is closed in the product topology.

theorem PiNat.isOpen_wordCylinder {α : Type u_1} [TopologicalSpace α] [DiscreteTopology α] (w : List α) : IsOpen (wordCylinder w)

Over a discrete alphabet, every word cylinder is open in the product topology.

theorem PiNat.isClopen_wordCylinder {α : Type u_1} [TopologicalSpace α] [DiscreteTopology α] (w : List α) : IsClopen (wordCylinder w)

Over a discrete alphabet, every word cylinder is clopen in the product topology.

theorem PiNat.measurableSet_wordCylinder {α : Type u_1} [MeasurableSpace α] [MeasurableSingletonClass α] (w : List α) : MeasurableSet (wordCylinder w)

Over an alphabet whose singletons are measurable, every word cylinder is measurable for the product σ-algebra.

theorem PiNat.isEmbedding_prependWord {α : Type u_1} [TopologicalSpace α] (w : List α) : Topology.IsEmbedding (prependWord w)

prependWord w is a topological embedding: its inverse on wordCylinder w forgets the first w.length coordinates.

theorem PiNat.isOpenEmbedding_prependWord {α : Type u_1} [TopologicalSpace α] [DiscreteTopology α] (w : List α) : Topology.IsOpenEmbedding (prependWord w)

Over a discrete alphabet, prependWord w is an open embedding onto the clopen set wordCylinder w.

theorem PiNat.isClosedEmbedding_prependWord {α : Type u_1} [TopologicalSpace α] [T1Space α] (w : List α) : Topology.IsClosedEmbedding (prependWord w)

Over a T₁ alphabet, prependWord w is a closed embedding onto wordCylinder w.

theorem PiNat.exists_tendsto_of_mem_wordCylinder {α : Type u_1} [TopologicalSpace α] {c : ℕ → List α} (hc : ∀ (m : ℕ), c m <+: c (m + 1)) (hlen : Filter.Tendsto (fun (m : ℕ) => (c m).length) Filter.atTop Filter.atTop) {γ : ℕ → ℕ → α} (hγ : ∀ (m : ℕ), γ m ∈ wordCylinder (c m)) : ∃ (β : ℕ → α), Filter.Tendsto γ Filter.atTop (nhds β)

Let the words c m increase in the prefix order, with lengths tending to infinity. Then any points γ m ∈ wordCylinder (c m) converge: eventually every coordinate of γ m is the letter that the words spell out at that position.

theorem PiNat.continuous_of_res_eq_of_dist_le {α : Type u_1} [TopologicalSpace α] [DiscreteTopology α] {X : Type u_2} [PseudoMetricSpace X] {F : ℕ → (ℕ → α) → X} {φ : (ℕ → α) → X} {ε : ℕ → ℝ} (hF : ∀ (n : ℕ) (x y : ℕ → α), res x n = res y n → F n x = F n y) (h : ∀ (n : ℕ) (x : ℕ → α), dist (F n x) (φ x) ≤ ε n) (hε : Filter.Tendsto ε Filter.atTop (nhds 0)) : Continuous φ

Over a discrete alphabet, a map φ of ℕ → α into a pseudometric space is continuous if it is the uniform limit of approximations F n such that F n x depends only on the first n coordinates res x n of x: F n x lies within ε n of φ x for every x, and ε n tends to 0.

The coordinate flip of Cantor space

def PiNat.flipAt (n : ℕ) : (ℕ → Bool) ≃ₜ (ℕ → Bool)

The homeomorphism of Cantor space ℕ → Bool negating the n-th coordinate.

theorem PiNat.flipAt_apply (n : ℕ) (x : ℕ → Bool) : (flipAt n) x = Function.update x n !x n

@[simp]

theorem PiNat.flipAt_apply_self (n : ℕ) (x : ℕ → Bool) : (flipAt n) x n = !x n

@[simp]

theorem PiNat.flipAt_apply_of_ne {m n : ℕ} (h : m ≠ n) (x : ℕ → Bool) : (flipAt n) x m = x m

@[simp]

theorem PiNat.symm_flipAt (n : ℕ) : (flipAt n).symm = flipAt n

@[simp]

theorem PiNat.flipAt_flipAt (n : ℕ) (x : ℕ → Bool) : (flipAt n) ((flipAt n) x) = x

theorem PiNat.flipAt_involutive (n : ℕ) : Function.Involutive ⇑(flipAt n)

The coordinate flip is an involution.

theorem PiNat.preimage_flipAt_wordCylinder (n : ℕ) (w : List Bool) : ⇑(flipAt n) ⁻¹' wordCylinder w = wordCylinder (w.modify n not)

The coordinate flip at n pulls the cylinder of w back to the cylinder of w with its n-th letter negated; when w.length ≤ n the cylinder is unchanged.

theorem PiNat.image_flipAt_wordCylinder (n : ℕ) (w : List Bool) : ⇑(flipAt n) '' wordCylinder w = wordCylinder (w.modify n not)

The coordinate flip at n maps the cylinder of w onto the cylinder of w with its n-th letter negated; when w.length ≤ n the cylinder is unchanged.

theorem PiNat.flipAt_prependWord_append_singleton (s : List Bool) (b : Bool) (x : ℕ → Bool) : (flipAt s.length) (prependWord (s ++ [b]) x) = prependWord (s ++ [!b]) x

The coordinate flip at s.length exchanges prependWord (s ++ [b]) x and prependWord (s ++ [!b]) x.

theorem PiNat.image_flipAt_wordCylinder_append_singleton (s : List Bool) (b : Bool) : ⇑(flipAt s.length) '' wordCylinder (s ++ [b]) = wordCylinder (s ++ [!b])

The coordinate flip at s.length maps the cylinder of s ++ [b] onto the cylinder of s ++ [!b], exchanging the two halves of the cylinder of s.