Showing S : Λ ⟶ ∑₂ is topological conjugacy with μ > 4

Stream: maths

[Attila Vajda]

I would like to learn to write this proof in Lean4,
to learn more about these concepts.

I got this exercise as part of a dynamical systems introductory course.

Any tips would help with what to learn to construct this proof.

Λ is Cantor set under logistic function f : μx(1-x), μ > 4
∑₂ is bi-infinite sequences with shift function S : ∑₂ ⟶ ∑₂

Conjugacy condition:
h ∘ f = S ∘ h
(I think this is the goal maybe)

  Λ ───f───> Λ
  |           |
 h|           |h
  ▼           ▼
  Σ₂ ───S───> Σ₂

[Kevin Buzzard]

Can you give much more precise definitions of $\Lambda$ and $\Sigma_2$? There are many meanings to "Cantor set", your function $f$ depends on an unspecified parameter $\mu$ and is unlikely to take a random Cantor set to itself, and you don't say the values that your sequences are taking.

[Attila Vajda]

Kevin Buzzard said:

Can you give much more precise definitions of $\Lambda$ and $\Sigma_2$? There are many meanings to "Cantor set", your function $f$ depends on an unspecified parameter $\mu$ and is unlikely to take a random Cantor set to itself, and you don't say the values that your sequences are taking.

Thank you for your message Kevin and yes! Here is more about $\Lambda$ and $\Sigma_2$.

It seems my textbook by Robert Devaney discusses all the components that make up a proof. I'm not yet sure why for $\mu > 4$ points escape the interval.

Λ

For $F_\mu = \mu x(1-x)$ with $\mu > 4$, the invariant Cantor set is:

$\Lambda = \bigcap_{n \ge 0} F_\mu^{-n}([0,1]).$

This is the set of points whose orbits never escape $[0,1]$.

∑₂

The space of infinite sequences of 0s and 1s is called the sequence space on the two symbols 0 and 1:

$\Sigma_2 = \{ s = (s_0 s_1 s_2 \dots) \mid s_j = 0 \text{ or } 1 \}.$

σ

The shift map is

$\sigma \colon \Sigma_2 \to \Sigma_2$

defined by $\sigma(s_0 s_1 s_2 \dots) = (s_1 s_2 s_3 \dots).$

S : Λ ⟶ ∑₂

"Thus, the itinerary of $x$ is an infinite sequence of 0’s and 1’s. That is, $S(x)$ is a point in the sequence space $\Sigma_2$. We think of $S$ as a map from $\Lambda$ to $\Sigma_2$. This map has several interesting properties." [Devaney]

conjugacy

I think the proof is to show the following diagram commutes:

$S \circ F_\mu = \sigma \circ S.$

"Topologically conjugate mappings are completely equivalent in terms of their dynamics." [Devaney]

Reference: An Introduction to Chaotic Dynamical Systems, Robert Devaney

Bildschirmfoto 2025-10-19 um 15.55.38.png
Bildschirmfoto 2025-10-19 um 15.55.28.png

[Aaron Liu]

Is $S$ strictly monotone if I put the lexographic order on $\Sigma_2$

[Aaron Liu]

Attila Vajda said:

It seems my textbook by Robert Devaney discusses all the components that make up a proof. I'm not yet sure why for $\mu > 4$ points escape the interval.

It's because $\mu > 4$ iff $F_\mu(1/2) > 1$

[Aaron Liu]

I think I am understanding what you want to do now but this function $S : \Lambda \to \Sigma_2$ is still pretty mysterious, can you give either a definition or some characteristic property that uniquely determines it?

[Attila Vajda]

Aaron Liu said:

I think I am understanding what you want to do now but this function $S : \Lambda \to \Sigma_2$ is still pretty mysterious, can you give either a definition or some characteristic property that uniquely determines it?

Oh I left the definition of S out, I think:

The itinerary of $x$ is a sequence $S(x) = s_0 s_1 s_2 \dots$, where
$s_j = 0$ if $F_\mu^j(x) \in I_0$, $s_j = 1$ if $F_\mu^j(x) \in I_1$.

And the proof is to show S is a homeomorphism, which sends Λ to ∑₂

  Λ  ───f───> Λ
  |           |
 S|           |S
  ▼           ▼
  Σ₂ ───σ───> Σ₂

• Vertical arrows = S (homeomorphism)
• Commutativity = S ∘ f = σ ∘ S
  both holds → topological conjugacy

Sorry if these don't yet make sense, but I am learning even from trying to explain this description!

[Aaron Liu]

Oh, what's $I_0$ and $I_1$? Can you prove that out of the two possibilities $F_\mu^j(x) \in I_0$ and $F_\mu^j(x) \in I_1$ exactly one of these happens?

[Attila Vajda]

Aaron Liu said:

Oh, what's $I_0$ and $I_1$? Can you prove that out of the two possibilities $F_\mu^j(x) \in I_0$ and $F_\mu^j(x) \in I_1$ exactly one of these happens?

I think I is the unit interval [0,1], and I₀ and I₁ are the set of points of the domain of f which don't escape near the peak y > 1 for the zeroth iteration.

Maybe x is in either because I₀ and I₁ are disjoint.

[Aaron Liu]

Attila Vajda said:

Aaron Liu said:

Oh, what's $I_0$ and $I_1$? Can you prove that out of the two possibilities $F_\mu^j(x) \in I_0$ and $F_\mu^j(x) \in I_1$ exactly one of these happens?

I think I is the unit interval [0,1], and I₀ and I₁ are the set of points of the domain of f which don't escape near the peak y > 1 for the zeroth iteration.

Maybe x is in either because I₀ and I₁ are disjoint.

Sorry, I still don't get it. What do you mean by "near"?

[Attila Vajda]

Aaron Liu said:

Attila Vajda said:

Aaron Liu said:

Oh, what's $I_0$ and $I_1$? Can you prove that out of the two possibilities $F_\mu^j(x) \in I_0$ and $F_\mu^j(x) \in I_1$ exactly one of these happens?

I think I is the unit interval [0,1], and I₀ and I₁ are the set of points of the domain of f which don't escape near the peak y > 1 for the zeroth iteration.

Maybe x is in either because I₀ and I₁ are disjoint.

Sorry, I still don't get it. What do you mean by "near"?

See the peak of this curve, apparently those points above the line don't return to [0,1]. I don't yet know what happens to those points, maybe "unstructured chaos" or "lost to infinity". They escape and tend to minus infinity.

Bildschirmfoto 2025-10-20 um 20.46.06.png

Bildschirmfoto 2025-10-20 um 21.09.47.png

I learnt perhaps σ(S(x)) = S(f(x)), because
σ(S(x)):
- σ starts the sequence S(x) makes from the second digit
S(f(x)) :
- f(x) is the first iteration, so it's sequence via S doesn't have the first digit of S(x)

S(x) = (b₀, b₁, b₂, …) reads the orbit starting at x (0th iteration).
S(f(x)) = (b₁, b₂, …) reads the orbit starting at the 1st iteration.
σ(S(x))=(b1​,b2​,…) shifts S(x) one

Here is a sketch in Lean4:

coinductive Σ₂
| cons : Fin 2 → Σ₂ → Σ₂

variable (μ : ℝ) (hμ : μ > 4)

def f (x : ℝ) := μ * x * (1-x)

def Λ := {x : ℝ | ∀ n, (f^[n] x) ∈ [0,1]}  -- invariant set under μ>4

def S (x : ℝ) : Σ₂ :=
  coinductive.cons (if x < 0.5 then 0 else 1) (S (f μ x))

def σ (s : Σ₂) : Σ₂ :=
  match s with
  | Σ₂.cons _ tail => tail

theorem conjugacy {x : ℝ} (xΛ : x ∈ Λ) :
  σ (S x) = S (f μ x) := by rfl

Also this seems like a nice idea:

Λ seems to have binary tree structure, as well as ∑₂, so would it be maybe meaningful to show

inductive 木  -- "tree"
| 葉 : 木                     -- leaf
| 節 : 木 → 木 → 木     -- node (branch)

Λ : 木 and ∑₂ : 木 → Λ ≅ ∑₂

[Aaron Liu]

ok after reading the thing I get it now

[Aaron Liu]

I don't know what kind of stuff you are trying to prove but here's a template that actually compiles

import Mathlib

variable (μ : ℝ)

def f (x : ℝ) : ℝ := μ * x * (1 - x)

theorem continuous_f : Continuous (f μ) := by
  sorry

def Λ : Set ℝ := { x | ∀ n, 0 ≤ (f μ)^[n] x }

theorem mapsto_f_Λ : Set.MapsTo (f μ) (Λ μ) (Λ μ) := by
  sorry

def rf : Λ μ → Λ μ := (mapsto_f_Λ μ).restrict

theorem Λ_subset_Icc (hμ : 0 < μ) : Λ μ ⊆ Set.Icc 0 1 := by
  sorry

theorem continuous_rf : Continuous (rf μ) := by
  sorry

abbrev BoolSeq : Type := Nat → Bool

def σ (x : BoolSeq) : BoolSeq := fun n => x (n + 1)

theorem continuous_σ : Continuous σ := by
  sorry

theorem surjective_σ : Function.Surjective σ := by
  sorry

noncomputable
def S (x : Λ μ) : BoolSeq := fun n => decide (2⁻¹ < ((rf μ)^[n] x).1)

theorem bijective_S (hμ : 4 < μ) : Function.Bijective (S μ) := by
  sorry

theorem continuous_S (hμ : 4 < μ) : Continuous (S μ) := by
  sorry

theorem isHomeomorph_S (hμ : 4 < μ) : IsHomeomorph (S μ) := by
  sorry

theorem semiconj_S_rf_σ (hμ : 4 < μ) : Function.Semiconj (S μ) (rf μ) σ := by
  sorry

theorem surjective_rf (hμ : 4 ≤ μ) : Function.Surjective (rf μ) := by
  sorry

[Attila Vajda]

Thank you for this template @Aaron Liu :dolphin: