Ternary Cantor Set

This file defines the Cantor ternary set and proves a few properties.

Main Definitions

• preCantorSet n: The order n pre-Cantor set, defined inductively as the union of the images under the functions (· / 3) and ((2 + ·) / 3), with preCantorSet 0 := Set.Icc 0 1, i.e. preCantorSet 0 is the unit interval [0,1].
• cantorSet: The ternary Cantor set, defined as the intersection of all pre-Cantor sets.
• cantorToTernary: given a number x in the Cantor set, returns its ternary representation (d₀, d₁, ...) consisting only of digits 0 and 2, such that x = 0.d₀d₁... (see ofDigits_cantorToTernary).
• ofDigits_zero_two_sequence_mem_cantorSet: any such sequence corresponds to a number in the Cantor set.
• ofDigits_zero_two_sequence_unique: such a representation is unique.

def preCantorSet : ℕ → Set ℝ

The order n pre-Cantor set, defined starting from [0, 1] and successively removing the middle third of each interval. Formally, the order n + 1 pre-Cantor set is the union of the images under the functions (· / 3) and ((2 + ·) / 3) of preCantorSet n.

Equations

• preCantorSet 0 = Set.Icc 0 1
• preCantorSet n.succ = (fun (x : ℝ) => x / 3) '' preCantorSet n ∪ (fun (x : ℝ) => (2 + x) / 3) '' preCantorSet n

@[simp]

theorem preCantorSet_zero : preCantorSet 0 = Set.Icc 0 1

@[simp]

theorem preCantorSet_succ (n : ℕ) : preCantorSet (n + 1) = (fun (x : ℝ) => x / 3) '' preCantorSet n ∪ (fun (x : ℝ) => (2 + x) / 3) '' preCantorSet n

def cantorSet : Set ℝ

The Cantor set is the subset of the unit interval obtained as the intersection of all pre-Cantor sets. This means that the Cantor set is obtained by iteratively removing the open middle third of each subinterval, starting from the unit interval [0, 1].

Equations

• cantorSet = ⋂ (n : ℕ), preCantorSet n

Simple Properties

theorem quarters_mem_preCantorSet (n : ℕ) : 1 / 4 ∈ preCantorSet n ∧ 3 / 4 ∈ preCantorSet n

theorem quarter_mem_preCantorSet (n : ℕ) : 1 / 4 ∈ preCantorSet n

theorem quarter_mem_cantorSet : 1 / 4 ∈ cantorSet

theorem zero_mem_preCantorSet (n : ℕ) : 0 ∈ preCantorSet n

theorem zero_mem_cantorSet : 0 ∈ cantorSet

theorem preCantorSet_antitone : Antitone preCantorSet

theorem preCantorSet_subset_unitInterval {n : ℕ} : preCantorSet n ⊆ Set.Icc 0 1

theorem cantorSet_subset_unitInterval : cantorSet ⊆ Set.Icc 0 1

The ternary Cantor set is a subset of [0,1].

theorem cantorSet_eq_union_halves : cantorSet = (fun (x : ℝ) => x / 3) '' cantorSet ∪ (fun (x : ℝ) => (2 + x) / 3) '' cantorSet

The ternary Cantor set satisfies the equation C = C / 3 ∪ (2 / 3 + C / 3).

theorem isClosed_preCantorSet (n : ℕ) : IsClosed (preCantorSet n)

The preCantor sets are closed.

theorem isClosed_cantorSet : IsClosed cantorSet

The ternary Cantor set is closed.

theorem isCompact_cantorSet : IsCompact cantorSet

The ternary Cantor set is compact.

The Cantor set as the set of 0–2 numbers in the ternary system.

theorem ofDigits_zero_two_sequence_mem_cantorSet {a : ℕ → Fin 3} (h : ∀ (n : ℕ), a n ≠ 1) : Real.ofDigits a ∈ cantorSet

If x = 0.d₀d₁... in base-3 (ternary), and none of the digits dᵢ is 1, then x belongs to the Cantor set.

theorem ofDigits_zero_two_sequence_unique {a b : ℕ → Fin 3} (ha : ∀ (n : ℕ), a n ≠ 1) (hb : ∀ (n : ℕ), b n ≠ 1) (h : Real.ofDigits a = Real.ofDigits b) : a = b

If two base-3 representations using only digits 0 and 2 define the same number, then the sequences must be equal. This uniqueness fails for general base-3 representations (e.g. 0.1000... = 0.0222...).

noncomputable def cantorStep (x : ℝ) : ℝ

Given x ∈ [0, 1/3] ∪ [2/3, 1] (i.e. a level of the Cantor set), this function rescales the interval containing x back to [0, 1]. Used to iteratively extract the ternary representation of x.

Equations

• cantorStep x = if x ∈ Set.Icc 0 (1 / 3) then 3 * x else 3 * x - 2

theorem cantorStep_mem_cantorSet {x : ℝ} (hx : x ∈ cantorSet) : cantorStep x ∈ cantorSet

noncomputable def cantorSequence (x : ℝ) : Stream' ℝ

The infinite sequence obtained by repeatedly applying cantorStep to x.

Equations

• cantorSequence x = Stream'.iterate cantorStep x

theorem cantorSequence_mem_cantorSet {x : ℝ} (hx : x ∈ cantorSet) (n : ℕ) : (cantorSequence x).get n ∈ cantorSet

noncomputable def cantorToBinary (x : ℝ) : Stream' Bool

Points of the Cantor set correspond to infinite paths in the full binary tree. at each level n, the set preCantorSet (n + 1) splits each interval in preCantorSet n into two parts. Given x ∈ cantorSet, the point x lies in one of the intervals of preCantorSet n. This function tracks which of the two intervals in preCantorSet (n + 1) contains x at each step, producing the corresponding path as a stream of booleans.

Equations

• cantorToBinary x = Stream'.map (fun (x : ℝ) => if x ∈ Set.Icc 0 (1 / 3) then false else true) (cantorSequence x)

noncomputable def cantorToTernary (x : ℝ) : Stream' (Fin 3)

Given x in the Cantor set, return its ternary representation (d₀, d₁, …) using only digits 0 and 2, such that x = 0.d₀d₁... in base-3.

Equations

• cantorToTernary x = Stream'.map (fun (x : Bool) => bif x then 2 else 0) (cantorToBinary x)

theorem ofDigits_bool_to_fin_three_mem_cantorSet (f : ℕ → Bool) : (Real.ofDigits fun (i : ℕ) => bif f i then 2 else 0) ∈ cantorSet

theorem cantorToTernary_ne_one {x : ℝ} {n : ℕ} : (cantorToTernary x).get n ≠ 1

theorem cantorSequence_get_succ (x : ℝ) (n : ℕ) : (cantorSequence x).get (n + 1) = 3 * ((cantorSequence x).get n - 3 ^ n * Real.ofDigitsTerm (cantorToTernary x).get n)

theorem cantorSequence_eq_self_sub_sum_cantorToTernary (x : ℝ) (n : ℕ) : (cantorSequence x).get n = (x - ∑ i ∈ Finset.range n, Real.ofDigitsTerm (cantorToTernary x).get i) * 3 ^ n

theorem ofDigits_cantorToTernary_sum_le {x : ℝ} (hx : x ∈ cantorSet) {n : ℕ} : ∑ i ∈ Finset.range n, Real.ofDigitsTerm (cantorToTernary x) i ≤ x

theorem le_ofDigits_cantorToTernary_sum {x : ℝ} (hx : x ∈ cantorSet) {n : ℕ} : x - 3⁻¹ ^ n ≤ ∑ i ∈ Finset.range n, Real.ofDigitsTerm (cantorToTernary x) i

theorem ofDigits_cantorToTernary {x : ℝ} (hx : x ∈ cantorSet) : Real.ofDigits (cantorToTernary x).get = x

theorem cantorSet_eq_zero_two_ofDigits : cantorSet = {x : ℝ | ∃ (a : ℕ → Fin 3), (∀ (i : ℕ), a i ≠ 1) ∧ Real.ofDigits a = x}

The Cantor set is homeomorphic to ℕ → Bool

noncomputable def cantorSetEquivNatToBool : ↑cantorSet ≃ (ℕ → Bool)

Canonical bijection between the Cantor set and infinite binary tree.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def cantorSetHomeomorphNatToBool : ↑cantorSet ≃ₜ (ℕ → Bool)

Canonical homeomorphism between the Cantor set and ℕ → Bool.

Equations

• cantorSetHomeomorphNatToBool = cantorSetHomeomorphNatToBool._proof_4.homeoOfEquivCompactToT2.symm

def cantorSpaceHomeomorphNatToCantorSpace : (ℕ → Bool) ≃ₜ (ℕ → ℕ → Bool)

The Cantor space is homeomorphic to a countable product of copies of itself.

Equations

• cantorSpaceHomeomorphNatToCantorSpace = (Homeomorph.piCongrLeft Nat.pairEquiv.symm).trans Homeomorph.piCurry