Aronson transform

TheoremExistence and uniqueness of the Aronson transform, general form#✓fully proved

Let \(n_0\) be a natural number and let \(\beta : \mathbb{N} \to \mathbb{N}\) be strictly increasing such that infinitely many integers \(m \ge n_0\) are not values of \(\beta\). Then there is exactly one sequence \(\alpha : \mathbb{N} \to \mathbb{N}\) such that \(\alpha\) is strictly increasing, \(\alpha_i \ge n_0\) for every \(i\), \(\alpha_0\) is the least integer \(m \ge n_0\) such that \(m = n_0\) holds exactly when \(m\) is a value of \(\beta\), and, for every \(i \ge 0\), \(\alpha_{i+1}\) is the least integer \(m > \alpha_i\) such that \(n_0 + i + 1 \in \{\alpha_0, \dots, \alpha_i, m\}\) holds exactly when \(m\) is a value of \(\beta\).

The values of \(\beta\) are not required to be at least \(n_0\).

MetaMathlibExt.aronsonTransform_existsUnique_general · 19 lines

theorem aronsonTransform_existsUnique_general
    (n₀ : ℕ)
    (β : ℕ → ℕ)
    (hβ_strictMono : StrictMono β)
    (hβ_complement : Set.Infinite {m : ℕ | n₀ ≤ m ∧ m ∉ Set.range β}) :
    ∃! α : ℕ → ℕ,
      StrictMono α ∧
      (∀ i, n₀ ≤ α i) ∧
      (((α 0 = n₀) ↔ α 0 ∈ Set.range β) ∧
        ∀ m, n₀ ≤ m →
          ((m = n₀) ↔ m ∈ Set.range β) →
          α 0 ≤ m) ∧
      ∀ i,
        let n := n₀ + i + 1
        ((((∃ j, j ≤ i ∧ α j = n) ∨ α (i + 1) = n) ↔
            α (i + 1) ∈ Set.range β) ∧
          ∀ m, α i < m →
            (((∃ j, j ≤ i ∧ α j = n) ∨ m = n) ↔ m ∈ Set.range β) →
            α (i + 1) ≤ m)

Used by 1

Used byExistence and uniqueness of the Aronson transform

TheoremExistence and uniqueness of the Aronson transform#✓fully proved

Let \(n_0\) be a natural number and let \(\beta : \mathbb{N} \to \mathbb{N}\) be strictly increasing with \(\beta_i \ge n_0\) for every \(i\), such that infinitely many integers \(m \ge n_0\) are not values of \(\beta\). Then there is exactly one sequence \(\alpha : \mathbb{N} \to \mathbb{N}\) such that \(\alpha\) is strictly increasing, \(\alpha_i \ge n_0\) for every \(i\), \(\alpha_0\) is the least integer \(m \ge n_0\) such that \(m = n_0\) holds exactly when \(m\) is a value of \(\beta\), and, for every \(i \ge 0\), \(\alpha_{i+1}\) is the least integer \(m > \alpha_i\) such that \(n_0 + i + 1 \in \{\alpha_0, \dots, \alpha_i, m\}\) holds exactly when \(m\) is a value of \(\beta\).

The hypothesis \(\beta_i \ge n_0\) is not used in the proof.

MetaMathlibExt.aronsonTransform_existsUnique · 21 lines

@[nolint unusedArguments]
theorem aronsonTransform_existsUnique
    (n₀ : ℕ)
    (β : ℕ → ℕ)
    (hβ_strictMono : StrictMono β)
    (hβ_lower : ∀ i, n₀ ≤ β i)
    (hβ_complement : Set.Infinite {m : ℕ | n₀ ≤ m ∧ m ∉ Set.range β}) :
    ∃! α : ℕ → ℕ,
      StrictMono α ∧
      (∀ i, n₀ ≤ α i) ∧
      (((α 0 = n₀) ↔ α 0 ∈ Set.range β) ∧
        ∀ m, n₀ ≤ m →
          ((m = n₀) ↔ m ∈ Set.range β) →
          α 0 ≤ m) ∧
      ∀ i,
        let n := n₀ + i + 1
        ((((∃ j, j ≤ i ∧ α j = n) ∨ α (i + 1) = n) ↔
            α (i + 1) ∈ Set.range β) ∧
          ∀ m, α i < m →
            (((∃ j, j ≤ i ∧ α j = n) ∨ m = n) ↔ m ∈ Set.range β) →
            α (i + 1) ≤ m)

Sources

• Benoit Cloitre, N. J. A. Sloane, and Matthew J. Vandermast, "Numerical Analogues of Aronson's Sequence," Journal of Integer Sequences 6 (2003), Article 03.2.2, Theorem ThAT1, lines 782–784 (transform defined lines 761–780), https://cs.uwaterloo.ca/journals/JIS/VOL6/Cloitre/cloitre2.tex

Uses 1

Proof usesExistence and uniqueness of the Aronson transform, general form

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.