Reciprocal sums of doubly exponential sequences

DefinitionPseudo-greedy remainder sequence#✓fully proved

For a real number \(r\), the remainder sequence \((x_n)_{n \ge 0}\) of the pseudo-greedy expansion of \(r\) is defined by \(x_0 = r\) and \(x_{n+1} = x_n - 1/a_n\), where \(a_n = \lfloor x_n^{-1} + 1 + 1/2 \rfloor\) is the integer nearest to \(x_n^{-1} + 1\), with halves rounded up.

Here \(0^{-1}\) and \(1/0\) are read as \(0\).

noncomputable def pseudoGreedyRemainder (r : ℝ) : ℕ → ℝ
  | 0 => r
  | n + 1 => pseudoGreedyRemainder r n -
      1 / (⌊(pseudoGreedyRemainder r n)⁻¹ + 1 + 1 / 2⌋ : ℝ)

Sources

• Junnosuke Koizumi, Irrationality of the Reciprocal Sum of Doubly Exponential Sequences, INTEGERS 26 (2026), Article A28, Section 2 (definitions of the pseudo-greedy expansion and its remainder sequence).

Used by 7

Used byPseudo-greedy expansion · Second term of the pseudo-greedy expansion of \(1\) · The pseudo-greedy expansion of 1 starts with 2 · Structure of the pseudo-greedy expansion of a rational · Gap sequence of the pseudo-greedy expansion · The first gap of the expansion of 1 vanishes · Remainder recursion

DefinitionPseudo-greedy expansion#✓fully proved

Let \(r\) be a real number with pseudo-greedy remainder sequence \((x_n)_{n \ge 0}\). The pseudo-greedy expansion of \(r\) is the integer sequence \(a_n = \lfloor x_n^{-1} + 1 + 1/2 \rfloor\) for \(n \ge 0\); that is, \(a_n\) is the integer nearest to \(x_n^{-1} + 1\), with halves rounded up.

Here \(0^{-1}\) is read as \(0\).

noncomputable def pseudoGreedyExpansion (r : ℝ) (n : ℕ) : ℤ :=
  ⌊(pseudoGreedyRemainder r n)⁻¹ + 1 + 1 / 2⌋

Sources

• Junnosuke Koizumi, Irrationality of the Reciprocal Sum of Doubly Exponential Sequences, INTEGERS 26 (2026), Article A28, Section 2 (definition of the pseudo-greedy expansion).

Uses 1 · Used by 9

Statement usesPseudo-greedy remainder sequence

Used byTails that are pseudo-greedy expansions · Convergence of the pseudo-greedy expansion · Second term of the pseudo-greedy expansion of \(1\) · The pseudo-greedy expansion of 1 starts with 2 · Structure of the pseudo-greedy expansion of a rational · Recursion for the pseudo-greedy expansion · Gap sequence of the pseudo-greedy expansion · The first gap of the expansion of 1 vanishes · Remainder recursion

DefinitionGap sequence of the pseudo-greedy expansion#✓fully proved

Let \(r\) be a real number, and let \((x_n)\) be the remainder sequence and \((a_n)\) the pseudo-greedy expansion of \(r\). The gap sequence of \(r\) is the real sequence \(\varepsilon_n = x_n^{-1} + 1 - a_n\) for \(n \ge 0\).

Here \(0^{-1}\) is read as \(0\).

noncomputable def pseudoGreedyGap (r : ℝ) (n : ℕ) : ℝ :=
  (pseudoGreedyRemainder r n)⁻¹ + 1 - pseudoGreedyExpansion r n

Sources

• Junnosuke Koizumi, Irrationality of the Reciprocal Sum of Doubly Exponential Sequences, INTEGERS 26 (2026), Article A28, Section 2 (definition of the gap sequence).

Uses 2 · Used by 7

Statement usesPseudo-greedy expansion · Pseudo-greedy remainder sequence

Used byEventual vanishing of the pseudo-greedy gaps of a rational number · Tails that are pseudo-greedy expansions · Koizumi's conjecture is equivalent to the Erdős–Graham question · Structure of the pseudo-greedy expansion of a rational · Recursion for the pseudo-greedy expansion · The first gap of the expansion of 1 vanishes · A vanishing gap stays zero

TheoremRemainder recursion#✓fully proved

For every real number \(r\) and every \(n \ge 0\), the remainder sequence \((x_n)\) and the pseudo-greedy expansion \((a_n)\) of \(r\) satisfy \(x_{n+1} = x_n - 1/a_n\).

Here \(1/0\) is read as \(0\).

theorem pseudoGreedyRemainder_succ (r : ℝ) (n : ℕ) :
    pseudoGreedyRemainder r (n + 1) =
      pseudoGreedyRemainder r n - 1 / (pseudoGreedyExpansion r n : ℝ)

Sources

• Junnosuke Koizumi, Irrationality of the Reciprocal Sum of Doubly Exponential Sequences, INTEGERS 26 (2026), Article A28, Section 2 (definition of the remainder sequence).

Uses 2 · Used by 1

Statement usesPseudo-greedy expansion · Pseudo-greedy remainder sequence

Used bySecond term of the pseudo-greedy expansion of \(1\)

TheoremThe pseudo-greedy expansion of 1 starts with 2#✓fully proved

The first term \(a_0\) of the pseudo-greedy expansion of \(1\) equals \(2\), the first Sylvester number.

theorem pseudoGreedyExpansion_one_zero : pseudoGreedyExpansion 1 0 = 2

Sources

• Junnosuke Koizumi, Irrationality of the Reciprocal Sum of Doubly Exponential Sequences, INTEGERS 26 (2026), Article A28, Example 1 (the expansion of 1 is the Sylvester sequence).

Uses 2 · Used by 2

Statement usesPseudo-greedy expansion

Proof usesPseudo-greedy remainder sequence

Used bySecond term of the pseudo-greedy expansion of \(1\) · The first gap of the expansion of 1 vanishes

TheoremSecond term of the pseudo-greedy expansion of \(1\)#✓fully proved

The pseudo-greedy expansion \((a_n)_{n \ge 0}\) of \(1\) satisfies \(a_1 = 3\).

The remainder after the first term \(a_0 = 2\) is \(1 - 1/2 = 1/2\).

theorem pseudoGreedyExpansion_one_one : pseudoGreedyExpansion 1 1 = 3

Sources

• Junnosuke Koizumi, Irrationality of the Reciprocal Sum of Doubly Exponential Sequences, INTEGERS 26 (2026), Article A28, Example 1 (the expansion of 1 is the Sylvester sequence).

Uses 4

Statement usesPseudo-greedy expansion

Proof usesThe pseudo-greedy expansion of 1 starts with 2 · Pseudo-greedy remainder sequence · Remainder recursion

TheoremThe first gap of the expansion of 1 vanishes#✓fully proved

The first term \(\varepsilon_0\) of the gap sequence of the pseudo-greedy expansion of \(1\) is \(0\): the first remainder is \(x_0 = 1\) and the first term of the expansion is \(a_0 = 2\), so \(\varepsilon_0 = x_0^{-1} + 1 - a_0 = 1 + 1 - 2 = 0\).

theorem pseudoGreedyGap_one_zero : pseudoGreedyGap 1 0 = 0

Sources

• Junnosuke Koizumi, Irrationality of the Reciprocal Sum of Doubly Exponential Sequences, INTEGERS 26 (2026), Article A28, Example 1 (ε_n = 0 for the expansion of 1).

Uses 4

Statement usesGap sequence of the pseudo-greedy expansion

Proof usesPseudo-greedy expansion · The pseudo-greedy expansion of 1 starts with 2 · Pseudo-greedy remainder sequence

TheoremRecovering a doubly exponential sequence from its reciprocal sum#●ready to prove

Let \(\beta \ge 0\) and \(r\) be real numbers, and let \((a_n)_{n \ge 0}\) be a sequence of positive integers with \(|a_n^2 / a_{n+1} - \beta| \le 1/3\) for all \(n\) and \(\sum_n 1 / a_n = r\). Write \(x_n = r - \sum_{k\lt n} 1 / a_k\). Then for every \(n\) with \(a_n \ge 8 (\beta + 1/3)^2\) we have \(a_n = \lfloor x_n^{-1} + \beta + 1/2 \rfloor\), that is, \(a_n\) is the integer nearest to \(x_n^{-1} + \beta\), with halves rounded up. Moreover, if \(a_n^2 / a_{n+1} \to \beta\), then \(|x_n^{-1} + \beta - a_n| \to 0\).

public theorem_wanted eq_round_inv_remainder_add {β r : ℝ} (hβ : 0 ≤ β) {a : ℕ → ℕ}
    (hpos : ∀ n, 0 < a n) (hratio : ∀ n, |(a n : ℝ) ^ 2 / a (n + 1) - β| ≤ 1 / 3)
    (hsum : HasSum (fun n => 1 / (a n : ℝ)) r) :
    (∀ n, 8 * (β + 1 / 3) ^ 2 ≤ (a n : ℝ) →
      (a n : ℤ) = ⌊(r - ∑ k ∈ Finset.range n, 1 / (a k : ℝ))⁻¹ + β + 1 / 2⌋) ∧
    (Tendsto (fun n => (a n : ℝ) ^ 2 / a (n + 1)) atTop (𝓝 β) →
      Tendsto (fun n => |(r - ∑ k ∈ Finset.range n, 1 / (a k : ℝ))⁻¹ + β - a n|) atTop (𝓝 0))

Sources

• Junnosuke Koizumi, Irrationality of the Reciprocal Sum of Doubly Exponential Sequences, INTEGERS 26 (2026), Article A28, Theorem 1.

TheoremCharacterization of the Sylvester sequence#●ready to prove

Let \((a_n)_{n \ge 0}\) be a sequence of positive integers with \(2/3 \le a_n^2 / a_{n+1} \le 4/3\) for all \(n\) and \(\sum_n 1 / a_n = 1\). Then \(a_n = s_n(1)\) for all \(n \ge 0\), where \((s_n(1))_{n \ge 0}\) is the generalized Sylvester sequence with parameter \(1\), that is, the Sylvester sequence \(2, 3, 7, 43, \ldots\).

public theorem_wanted eq_sylvester_of_ratio_mem_of_hasSum_one {a : ℕ → ℕ}
    (hpos : ∀ n, 0 < a n)
    (hratio : ∀ n, 2 / 3 ≤ (a n : ℝ) ^ 2 / a (n + 1) ∧ (a n : ℝ) ^ 2 / a (n + 1) ≤ 4 / 3)
    (hsum : HasSum (fun n => 1 / (a n : ℝ)) 1) :
    ∀ n, a n = Nat.generalizedSylvester 1 n

Sources

• Junnosuke Koizumi, Irrationality of the Reciprocal Sum of Doubly Exponential Sequences, INTEGERS 26 (2026), Article A28, Corollary 1.

Uses 1

Statement usesGeneralized Sylvester sequence

TheoremCharacterization of the denominators of the Millin series#●ready to prove

Let \((a_n)_{n \ge 0}\) be a sequence of positive integers with \(a_n^2 / a_{n+1} \le 2/3\) for all \(n\) and \(\sum_n 1 / a_n = (5 - \sqrt 5) / 2\). Then \(a_n = F_{2^{n+1}}\) for all \(n \ge 0\), where \(F_k\) is the \(k\)-th Fibonacci number (\(F_0 = 0\), \(F_1 = 1\)); that is, \(a\) is the sequence \(F_2, F_4, F_8, \ldots\).

public theorem_wanted eq_fib_two_pow_of_ratio_le_of_hasSum_millin {a : ℕ → ℕ}
    (hpos : ∀ n, 0 < a n) (hratio : ∀ n, (a n : ℝ) ^ 2 / a (n + 1) ≤ 2 / 3)
    (hsum : HasSum (fun n => 1 / (a n : ℝ)) ((5 - √5) / 2)) :
    ∀ n, a n = Nat.fib (2 ^ (n + 1))

Sources

• Junnosuke Koizumi, Irrationality of the Reciprocal Sum of Doubly Exponential Sequences, INTEGERS 26 (2026), Article A28, Corollary 2.

TheoremDoubly exponential floors are Type 2 irrationality sequences for all but countably many bases#●ready to prove

Doubly exponential floors are Type 2 irrationality sequences for all but countably many bases. For all real numbers \(\alpha > 1\) outside a countable set, the sequence \((\lfloor \alpha^{2^{n+1}} \rfloor)_{n \ge 0}\) is a Type 2 irrationality sequence: for every sequence \((b_n)_{n \ge 0}\) of positive integers with \(b_n / \lfloor \alpha^{2^{n+1}} \rfloor \to 1\), the series \(\sum_n 1 / b_n\) does not converge to a rational number.

public theorem_wanted countable_not_type2IrrationalitySequence_floor_pow_two_pow :
    Set.Countable {α : ℝ | 1 < α ∧ ¬∀ b : ℕ → ℕ, (∀ n, 0 < b n) →
      Tendsto (fun n => (b n : ℝ) / ⌊α ^ 2 ^ (n + 1)⌋₊) atTop (𝓝 1) →
        ∀ q : ℚ, ¬HasSum (fun n => 1 / (b n : ℝ)) q}

Sources

• Junnosuke Koizumi, Irrationality of the Reciprocal Sum of Doubly Exponential Sequences, INTEGERS 26 (2026), Article A28, Theorem 2 and the definition of Type 2 irrationality sequences preceding it.

TheoremConvergence of the pseudo-greedy expansion#●ready to prove

For every real number \(r > 0\), the pseudo-greedy expansion \((a_n)_{n \ge 0}\) of \(r\) satisfies \(\sum_n 1 / a_n = r\).

public theorem_wanted hasSum_one_div_pseudoGreedyExpansion {r : ℝ} (hr : 0 < r) :
    HasSum (fun n => 1 / (pseudoGreedyExpansion r n : ℝ)) r

Sources

• Junnosuke Koizumi, Irrationality of the Reciprocal Sum of Doubly Exponential Sequences, INTEGERS 26 (2026), Article A28, Lemma 1.

Uses 1

Statement usesPseudo-greedy expansion

TheoremRecursion for the pseudo-greedy expansion#●ready to prove

Let \(r > 0\) be a real number, and let \((a_n)\) be its pseudo-greedy expansion and \((\varepsilon_n)\) its gap sequence. Then for every \(n \ge 0\),

\[a_{n+1} = \frac{a_n^2}{1 - \varepsilon_n} - a_n + (1 - \varepsilon_{n+1}).\]

public theorem_wanted pseudoGreedyExpansion_succ_eq {r : ℝ} (hr : 0 < r) (n : ℕ) :
    (pseudoGreedyExpansion r (n + 1) : ℝ) =
      1 / (1 - pseudoGreedyGap r n) * (pseudoGreedyExpansion r n : ℝ) ^ 2 -
        pseudoGreedyExpansion r n + (1 - pseudoGreedyGap r (n + 1))

Sources

• Junnosuke Koizumi, Irrationality of the Reciprocal Sum of Doubly Exponential Sequences, INTEGERS 26 (2026), Article A28, Lemma 2.

Uses 2

Statement usesPseudo-greedy expansion · Gap sequence of the pseudo-greedy expansion

TheoremA vanishing gap stays zero#●ready to prove

Let \(r > 0\) be a real number and let \((\varepsilon_n)\) be the gap sequence of its pseudo-greedy expansion. For every \(n \ge 0\), if \(\varepsilon_n = 0\), then \(\varepsilon_{n+1} = 0\).

public theorem_wanted pseudoGreedyGap_succ_eq_zero {r : ℝ} (hr : 0 < r) {n : ℕ}
    (h : pseudoGreedyGap r n = 0) : pseudoGreedyGap r (n + 1) = 0

Sources

• Junnosuke Koizumi, Irrationality of the Reciprocal Sum of Doubly Exponential Sequences, INTEGERS 26 (2026), Article A28, Lemma 3.

Uses 1

Statement usesGap sequence of the pseudo-greedy expansion

TheoremStructure of the pseudo-greedy expansion of a rational#●ready to prove

Let \(p\) and \(q\) be positive integers, let \(r = p/q\), and let \((x_n)\), \((a_n)\) and \((\varepsilon_n)\) be the remainder sequence, the pseudo-greedy expansion and the gap sequence of \(r\). Put \(d_n = q a_0 a_1 \cdots a_{n-1}\) (so \(d_0 = q\)). Then there are positive integers \(c_n\) and integers \(e_n\) (\(n \ge 0\)) such that for every \(n\) we have \(x_n = c_n / d_n\), \(\varepsilon_n = e_n / c_n\), \(e_n \equiv d_n \pmod{c_n}\), \(-c_n/2 \le e_n < c_n/2\), \(a_n = (d_n - e_n)/c_n + 1\), \(c_{n+1} = c_n - e_n\) and \(d_{n+1} = d_n a_n\). Moreover, as \(n \to \infty\), \(c_n = O(a_0 \cdots a_{n-1} / a_n)\) and \(c_n = O(1.5^n)\).

public theorem_wanted pseudoGreedyExpansion_rational_structure {p q : ℕ} (hp : 0 < p)
    (hq : 0 < q) :
    let r : ℝ := p / q
    let a : ℕ → ℤ := pseudoGreedyExpansion r
    let d : ℕ → ℤ := fun n => q * ∏ k ∈ Finset.range n, a k
    ∃ (c : ℕ → ℕ) (e : ℕ → ℤ),
      (∀ n, 0 < c n ∧ pseudoGreedyRemainder r n = (c n : ℝ) / d n ∧
        pseudoGreedyGap r n = (e n : ℝ) / c n) ∧
      (∀ n, e n ≡ d n [ZMOD c n] ∧ -(c n : ℝ) / 2 ≤ e n ∧ (e n : ℝ) < c n / 2 ∧
        (a n : ℝ) = (d n - e n : ℝ) / c n + 1 ∧ (c (n + 1) : ℤ) = c n - e n ∧
        d (n + 1) = d n * a n) ∧
      (fun n => (c n : ℝ)) =O[atTop] (fun n => (∏ k ∈ Finset.range n, (a k : ℝ)) / a n) ∧
      (fun n => (c n : ℝ)) =O[atTop] (fun n => (1.5 : ℝ) ^ n)

Sources

• Junnosuke Koizumi, Irrationality of the Reciprocal Sum of Doubly Exponential Sequences, INTEGERS 26 (2026), Article A28, Lemma 4.

Uses 3

Statement usesPseudo-greedy expansion · Gap sequence of the pseudo-greedy expansion · Pseudo-greedy remainder sequence

TheoremEventual vanishing of the pseudo-greedy gaps of a rational number#●ready to prove

Let \(r\) be a positive rational number and let \((\varepsilon_n)_{n \ge 0}\) be the gap sequence of the pseudo-greedy expansion of \(r\). Suppose that \(\liminf_n \varepsilon_n \prod_{k\lt n} (1 - \varepsilon_k) \ge 0\), that is, for every \(\delta > 0\) we have \(\varepsilon_n \prod_{k\lt n} (1 - \varepsilon_k) \ge -\delta\) for all sufficiently large \(n\); or that \(\varepsilon_n \ge 0\) for all sufficiently large \(n\). Then \(\varepsilon_n = 0\) for all sufficiently large \(n\).

public theorem_wanted eventually_pseudoGreedyGap_eq_zero {r : ℚ} (hr : 0 < r)
    (h : (∀ δ : ℝ, 0 < δ → ∀ᶠ n in atTop,
        -δ ≤ pseudoGreedyGap r n * ∏ k ∈ Finset.range n, (1 - pseudoGreedyGap r k)) ∨
      ∀ᶠ n in atTop, 0 ≤ pseudoGreedyGap r n) :
    ∀ᶠ n in atTop, pseudoGreedyGap r n = 0

Sources

• Junnosuke Koizumi, Irrationality of the Reciprocal Sum of Doubly Exponential Sequences, INTEGERS 26 (2026), Article A28, Proposition 1.

Uses 1

Statement usesGap sequence of the pseudo-greedy expansion

TheoremTails that are pseudo-greedy expansions#●ready to prove

Let \((a_n)_{n \ge 0}\) be a sequence of positive integers with \(a_n^2 / a_{n+1} \to 1\) such that \(\sum_n 1 / a_n\) converges. Then there is a natural number \(N\) such that, with \(r = \sum_{k \ge 0} 1 / a_{N+k}\), the tail \((a_{N+n})_{n \ge 0}\) is the pseudo-greedy expansion of \(r\), and the gap sequence of this expansion tends to \(0\).

public theorem_wanted exists_tail_eq_pseudoGreedyExpansion {a : ℕ → ℕ} (hpos : ∀ n, 0 < a n)
    (hratio : Tendsto (fun n => (a n : ℝ) ^ 2 / a (n + 1)) atTop (𝓝 1))
    (hsum : Summable fun n => 1 / (a n : ℝ)) :
    ∃ N : ℕ,
      (∀ n, (a (N + n) : ℤ) = pseudoGreedyExpansion (∑' k, 1 / (a (N + k) : ℝ)) n) ∧
      Tendsto (pseudoGreedyGap (∑' k, 1 / (a (N + k) : ℝ))) atTop (𝓝 0)

Sources

• Junnosuke Koizumi, Irrationality of the Reciprocal Sum of Doubly Exponential Sequences, INTEGERS 26 (2026), Article A28, Corollary 3.

Uses 2

Statement usesPseudo-greedy expansion · Gap sequence of the pseudo-greedy expansion

TheoremErdős–Straus and Badea criterion for the Sylvester recurrence#●ready to prove

Let \((a_n)_{n \ge 0}\) be a sequence of positive integers with \(a_n^2 / a_{n+1} \to 1\) such that \(\sum_n 1 / a_n\) converges to a rational number. Suppose that \(\liminf_n (a_0 \cdots a_{n-1} / a_n)(1 - a_n^2 / a_{n+1}) \ge 0\), that is, for every \(\delta > 0\) this quantity is at least \(-\delta\) for all sufficiently large \(n\); or that \(a_{n+1} \ge a_n^2 - a_n + 1\) for all sufficiently large \(n\). Then \(a_{n+1} = a_n^2 - a_n + 1\) for all sufficiently large \(n\).

public theorem_wanted eventually_sylvester_recurrence_of_rational_sum {a : ℕ → ℕ}
    (hpos : ∀ n, 0 < a n)
    (hratio : Tendsto (fun n => (a n : ℝ) ^ 2 / a (n + 1)) atTop (𝓝 1))
    (hrat : ∃ q : ℚ, HasSum (fun n => 1 / (a n : ℝ)) q)
    (h : (∀ δ : ℝ, 0 < δ → ∀ᶠ n in atTop,
        -δ ≤ (∏ k ∈ Finset.range n, (a k : ℝ)) / a n * (1 - (a n : ℝ) ^ 2 / a (n + 1))) ∨
      ∀ᶠ n in atTop, a n ^ 2 - a n + 1 ≤ a (n + 1)) :
    ∀ᶠ n in atTop, a (n + 1) = a n ^ 2 - a n + 1

Sources

• Junnosuke Koizumi, Irrationality of the Reciprocal Sum of Doubly Exponential Sequences, INTEGERS 26 (2026), Article A28, Corollary 4.

TheoremKoizumi's conjecture is equivalent to the Erdős–Graham question#●ready to prove

The following are equivalent. (1) For every positive rational number \(r\) whose pseudo-greedy gap sequence \((\varepsilon_n)_{n \ge 0}\) tends to \(0\), we have \(\varepsilon_n = 0\) for all sufficiently large \(n\). (2) Every sequence \((a_n)_{n \ge 0}\) of positive integers with \(a_n^2 / a_{n+1} \to 1\) such that \(\sum_n 1 / a_n\) converges to a rational number satisfies \(a_{n+1} = a_n^2 - a_n + 1\) for all sufficiently large \(n\).

public theorem_wanted pseudoGreedy_conjecture_iff_erdos_graham_question :
    (∀ r : ℚ, 0 < r → Tendsto (pseudoGreedyGap r) atTop (𝓝 0) →
        ∀ᶠ n in atTop, pseudoGreedyGap r n = 0) ↔
      ∀ a : ℕ → ℕ, (∀ n, 0 < a n) →
        Tendsto (fun n => (a n : ℝ) ^ 2 / a (n + 1)) atTop (𝓝 1) →
        (∃ q : ℚ, HasSum (fun n => 1 / (a n : ℝ)) q) →
        ∀ᶠ n in atTop, a (n + 1) = a n ^ 2 - a n + 1

Sources

• Junnosuke Koizumi, Irrationality of the Reciprocal Sum of Doubly Exponential Sequences, INTEGERS 26 (2026), Article A28, Theorem 3, with Conjecture 1 and Question 1.

Uses 1

Statement usesGap sequence of the pseudo-greedy expansion

7 fully proved12 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.