Lüroth series

DefinitionFirst Lüroth digit#✓fully proved

For a real number \(x\), the first Lüroth digit of \(x\) is the natural number \(d_1(x) = \lfloor 1/x \rfloor + 1\), where \(\lfloor \cdot \rfloor\) is the floor truncated at \(0\) and \(1/0 = 0\). For \(x \in (0, 1]\) this is the usual digit and is at least \(2\); for \(x \le 0\) and for \(x > 1\) it equals \(1\).

noncomputable def lurothDigit (x : ℝ) : ℕ :=
  ⌊1 / x⌋₊ + 1

Sources

• Dmitry Kleinbock and Yuqing Zhang, Metrical Properties of Functions of Consecutive Digits in Lüroth Series, INTEGERS 24 (2024), Article A67, Section 2.

Used by 10

Used byFirst Lüroth digit of 1/2 · First Lüroth digit of 1 · Lüroth digits · The Lüroth digits of 1 · The Lüroth map shifts the digits · Lüroth map · The Lüroth map at 1/2 · The Lüroth orbit of \(27/71\) has period two · The Lüroth map fixes 1 · The Lüroth map fixes 0

DefinitionLüroth map#✓fully proved

For a real number \(x\) with first Lüroth digit \(d = d_1(x)\), the Lüroth map is \(L(x) = d(d - 1)x - (d - 1)\).

noncomputable def lurothMap (x : ℝ) : ℝ :=
  (lurothDigit x : ℝ) * ((lurothDigit x : ℝ) - 1) * x - ((lurothDigit x : ℝ) - 1)

Sources

• Dmitry Kleinbock and Yuqing Zhang, Metrical Properties of Functions of Consecutive Digits in Lüroth Series, INTEGERS 24 (2024), Article A67, Section 2.

Uses 1 · Used by 7

Statement usesFirst Lüroth digit

Used byLüroth digits · The Lüroth digits of 1 · The Lüroth map shifts the digits · The Lüroth map at 1/2 · The Lüroth orbit of \(27/71\) has period two · The Lüroth map fixes 1 · The Lüroth map fixes 0

DefinitionLüroth digits#✓fully proved

For a real number \(x\) and \(n \ge 1\), the \(n\)-th Lüroth digit of \(x\) is \(d_n(x) = d_1(L^{n-1}(x))\), where \(d_1\) is the first Lüroth digit, \(L\) is the Lüroth map and \(L^{n-1}\) is its \((n-1)\)-fold iterate (\(L^0\) is the identity).

The digit sequence is indexed from \(0\): its term of index \(k\) is \(d_1(L^k(x)) = d_{k+1}(x)\).

noncomputable def lurothDigitSeq (x : ℝ) (k : ℕ) : ℕ :=
  lurothDigit (lurothMap^[k] x)

Sources

• Dmitry Kleinbock and Yuqing Zhang, Metrical Properties of Functions of Consecutive Digits in Lüroth Series, INTEGERS 24 (2024), Article A67, Section 2.

Uses 2 · Used by 16

Statement usesFirst Lüroth digit · Lüroth map

Used byRecognising Lüroth convergents · A Lüroth triple from the expansion of \(1\) · Lower bound for the measure of large Lüroth digit values · Lüroth convergents approximate from below · The Lüroth digits of 1 · The Lüroth map shifts the digits · Lüroth convergent triples · Lüroth well approximable numbers · Lüroth well approximable numbers lie in \((0, 1)\) · Borel–Cantelli dichotomy for Lüroth cylinder events · Zero-one law for functions of consecutive Lüroth digits · Integral zero-one law for functions of consecutive Lüroth digits · Measure of Lüroth cylinders · Borel–Bernstein theorem for Lüroth digits · Upper bound for the measure of a Lüroth digit superlevel set · Zero-one law for weighted products of consecutive Lüroth digits

TheoremFirst Lüroth digit of 1#✓fully proved

The first Lüroth digit of \(1\) is \(d_1(1) = 2\).

theorem lurothDigit_one : lurothDigit 1 = 2

Sources

• Dmitry Kleinbock and Yuqing Zhang, Metrical Properties of Functions of Consecutive Digits in Lüroth Series, INTEGERS 24 (2024), Article A67, Section 2 (definition of d₁).

Uses 1 · Used by 2

Statement usesFirst Lüroth digit

Used byThe Lüroth digits of 1 · The Lüroth map fixes 1

TheoremFirst Lüroth digit of 1/2#✓fully proved

The first Lüroth digit of \(1/2\) is \(d_1(1/2) = 3\).

theorem lurothDigit_half : lurothDigit (1 / 2) = 3

Sources

• Dmitry Kleinbock and Yuqing Zhang, Metrical Properties of Functions of Consecutive Digits in Lüroth Series, INTEGERS 24 (2024), Article A67, Section 2 (definition of d₁).

Uses 1 · Used by 1

Statement usesFirst Lüroth digit

Used byThe Lüroth map at 1/2

TheoremThe Lüroth map fixes 1#✓fully proved

The Lüroth map \(L\) satisfies \(L(1) = 1\).

theorem lurothMap_one : lurothMap 1 = 1

Sources

• Dmitry Kleinbock and Yuqing Zhang, Metrical Properties of Functions of Consecutive Digits in Lüroth Series, INTEGERS 24 (2024), Article A67, Section 2 (definition of L).

Uses 3 · Used by 1

Statement usesLüroth map

Proof usesFirst Lüroth digit · First Lüroth digit of 1

Used byThe Lüroth digits of 1

TheoremThe Lüroth map at 1/2#✓fully proved

The Lüroth map \(L\) sends \(1/2\) to \(1\): \(L(1/2) = 1\).

theorem lurothMap_half : lurothMap (1 / 2) = 1

Sources

• Dmitry Kleinbock and Yuqing Zhang, Metrical Properties of Functions of Consecutive Digits in Lüroth Series, INTEGERS 24 (2024), Article A67, Section 2 (definition of L).

Uses 3

Statement usesLüroth map

Proof usesFirst Lüroth digit · First Lüroth digit of 1/2

TheoremThe Lüroth map fixes 0#✓fully proved

The Lüroth map \(L\) satisfies \(L(0) = 0\).

theorem lurothMap_zero : lurothMap 0 = 0

Sources

• Dmitry Kleinbock and Yuqing Zhang, Metrical Properties of Functions of Consecutive Digits in Lüroth Series, INTEGERS 24 (2024), Article A67, Section 2 (definition of L).

Uses 2

Statement usesLüroth map

Proof usesFirst Lüroth digit

TheoremThe Lüroth map shifts the digits#✓fully proved

For every real number \(x\) and every \(n \ge 1\), the \(n\)-th Lüroth digit of \(L(x)\), where \(L\) is the Lüroth map, is the \((n+1)\)-st Lüroth digit of \(x\): \(d_n(L(x)) = d_{n+1}(x)\).

theorem lurothDigitSeq_succ (x : ℝ) (k : ℕ) :
    lurothDigitSeq x (k + 1) = lurothDigitSeq (lurothMap x) k

Sources

• Dmitry Kleinbock and Yuqing Zhang, Metrical Properties of Functions of Consecutive Digits in Lüroth Series, INTEGERS 24 (2024), Article A67, Section 2 (definition of d_n).

Uses 3

Statement usesLüroth digits · Lüroth map

Proof usesFirst Lüroth digit

TheoremMeasure of Lüroth cylinders#●ready to prove

Write \(d_k(x)\) for the \(k\)-th Lüroth digit of \(x\). For every \(n \in \mathbb{N}\) and all natural numbers \(c_1, \dots, c_n\), the set \(\{x \in (0, 1] : d_j(x) = c_j \text{ for } 1 \le j \le n\}\) has Lebesgue measure \(\prod_{j=1}^{n} \frac{1}{c_j (c_j - 1)}\), with the convention \(1/0 = 0\); in particular both sides vanish when some \(c_j < 2\).

public theorem_wanted volume_lurothCylinder {n : ℕ} (c : Fin n → ℕ) :
    volume {x ∈ Set.Ioc (0 : ℝ) 1 | ∀ j : Fin n, lurothDigitSeq x j = c j} =
      ∏ j, ENNReal.ofReal (1 / ((c j : ℝ) * ((c j : ℝ) - 1)))

Sources

• Dmitry Kleinbock and Yuqing Zhang, Metrical Properties of Functions of Consecutive Digits in Lüroth Series, INTEGERS 24 (2024), Article A67, Proposition 1, (10).

Uses 1

Statement usesLüroth digits

TheoremBorel–Bernstein theorem for Lüroth digits#●ready to prove

Let \((\Psi(n))_{n \ge 0}\) be a sequence of positive reals, write \(d_k(x)\) for the \(k\)-th Lüroth digit of \(x\), and let \(E\) be the set of \(x \in (0, 1]\) such that \(d_{n+1}(x) \ge \Psi(n)\) for infinitely many \(n\). If \(\sum_{n \ge 0} 1 / \Psi(n) < \infty\) then \(E\) has Lebesgue measure \(0\), and if \(\sum_{n \ge 0} 1 / \Psi(n) = \infty\) then \(E\) has Lebesgue measure \(1\).

The paper quotes this result from Jager and de Vroedt (its reference [3]).

public theorem_wanted volume_lurothDigit_ge_zero_one (Ψ : ℕ → ℝ) (hΨ : ∀ n, 0 < Ψ n) :
    let E := {x ∈ Set.Ioc (0 : ℝ) 1 | ∃ᶠ n in atTop, Ψ n ≤ lurothDigitSeq x n}
    (Summable (fun n => (Ψ n)⁻¹) → volume E = 0) ∧
      (¬ Summable (fun n => (Ψ n)⁻¹) → volume E = 1)

Sources

• Dmitry Kleinbock and Yuqing Zhang, Metrical Properties of Functions of Consecutive Digits in Lüroth Series, INTEGERS 24 (2024), Article A67, Theorem 1.

Uses 1

Statement usesLüroth digits

TheoremZero-one law for weighted products of consecutive Lüroth digits#●ready to prove

Let \(m \ge 1\), let \(t_0, \dots, t_{m-1}\) be positive reals, let \(T = \max_i t_i\) and let \(\ell\) be the number of indices \(j\) with \(t_j = T\). Let \((\Psi(n))_{n \ge 0}\) be a sequence of positive reals for which there is \(c > 1\) with \(\Psi(n) \ge c\) for all sufficiently large \(n\) (equivalently, \(\liminf_n \Psi(n) > 1\)). Write \(d_k(x)\) for the \(k\)-th Lüroth digit of \(x\) and let \(E\) be the set of \(x \in (0, 1]\) such that \(\prod_{i=0}^{m-1} d_{n+i+1}(x)^{t_i} \ge \Psi(n)\) for infinitely many \(n\). If the series \(\sum_{n \ge 0} (\log \Psi(n))^{\ell - 1} / \Psi(n)^{1/T}\) converges then \(E\) has Lebesgue measure \(0\), and if it diverges then \(E\) has Lebesgue measure \(1\).

The paper quotes this result from Brown-Sarre, Robert and Hussain (its reference [2]).

public theorem_wanted volume_lurothWeightedProduct_ge_zero_one {m : ℕ} (hm : 0 < m)
    (t : Fin m → ℝ) (ht : ∀ i, 0 < t i) (Ψ : ℕ → ℝ) (hΨ : ∀ n, 0 < Ψ n)
    (hlim : ∃ c : ℝ, 1 < c ∧ ∀ᶠ n in atTop, c ≤ Ψ n) :
    let T := ⨆ i, t i
    let ℓ := (Finset.univ.filter fun j => t j = T).card
    let E := {x ∈ Set.Ioc (0 : ℝ) 1 |
      ∃ᶠ n in atTop, Ψ n ≤ ∏ i : Fin m, (lurothDigitSeq x (n + i) : ℝ) ^ t i}
    (Summable (fun n => Real.log (Ψ n) ^ (ℓ - 1) / Ψ n ^ (1 / T)) → volume E = 0) ∧
      (¬ Summable (fun n => Real.log (Ψ n) ^ (ℓ - 1) / Ψ n ^ (1 / T)) → volume E = 1)

Sources

• Dmitry Kleinbock and Yuqing Zhang, Metrical Properties of Functions of Consecutive Digits in Lüroth Series, INTEGERS 24 (2024), Article A67, Theorem 2, with T and ℓ(t) from (2).

Uses 1

Statement usesLüroth digits

TheoremZero-one law for functions of consecutive Lüroth digits#●ready to prove

Let \(m \in \mathbb{N}\), let \(F\) be a real-valued function on \(m\)-tuples of natural numbers and let \((\Psi(n))_{n \ge 0}\) be a real sequence. For \(y \in \mathbb{R}\) put

\[H(y) = \sum_{a} \prod_{i=1}^{m} \frac{1}{a_i (a_i - 1)} \in [0, \infty],\]

the sum running over the \(a = (a_1, \dots, a_m) \in \mathbb{N}^m\) with every \(a_i \ge 2\) and \(F(a) \ge y\). Write \(d_k(x)\) for the \(k\)-th Lüroth digit of \(x\) and let \(E\) be the set of \(x \in (0, 1]\) such that \(F(d_{n+1}(x), \dots, d_{n+m}(x)) \ge \Psi(n)\) for infinitely many \(n\). If \(\sum_{n \ge 0} H(\Psi(n)) < \infty\) then \(E\) has Lebesgue measure \(0\), and if \(\sum_{n \ge 0} H(\Psi(n)) = \infty\) then \(E\) has Lebesgue measure \(1\).

Unlike the paper, \(F\) and \(\Psi\) need not be positive.

public theorem_wanted volume_lurothConsecutiveDigits_zero_one {m : ℕ}
    (F : (Fin m → ℕ) → ℝ) (Ψ : ℕ → ℝ) :
    let H : ℝ → ℝ≥0∞ := fun y => ∑' d : Fin m → ℕ,
      if (∀ i, 2 ≤ d i) ∧ y ≤ F d then ∏ i, ENNReal.ofReal (1 / ((d i : ℝ) * ((d i : ℝ) - 1)))
      else 0
    let E := {x ∈ Set.Ioc (0 : ℝ) 1 |
      ∃ᶠ n in atTop, Ψ n ≤ F (fun i => lurothDigitSeq x (n + i))}
    (∑' n, H (Ψ n) < ∞ → volume E = 0) ∧ (∑' n, H (Ψ n) = ∞ → volume E = 1)

Sources

• Dmitry Kleinbock and Yuqing Zhang, Metrical Properties of Functions of Consecutive Digits in Lüroth Series, INTEGERS 24 (2024), Article A67, Theorem 3, with H from (4).

Uses 1

Statement usesLüroth digits

TheoremIntegral zero-one law for functions of consecutive Lüroth digits#●ready to prove

Let \(m \in \mathbb{N}\) and let \(F : \mathbb{R}^m \to \mathbb{R}\) be a measurable function that is positive on \([2, \infty)^m\) and non-decreasing there for the coordinatewise order. Let \(M \in \mathbb{R}\) satisfy \(F(x) \le M F(\lfloor x_1 \rfloor, \dots, \lfloor x_m \rfloor)\) for every \(x \in [2, \infty)^m\), and for \(y \in \mathbb{R}\) put

\[G(y) = \int_{\{x \in [2, \infty)^m : F(x) \ge y\}} \prod_{i=1}^{m} \frac{1}{x_i^2} \, dx.\]

Let \((\Psi(n))_{n \ge 0}\) be a real sequence, write \(d_k(x)\) for the \(k\)-th Lüroth digit of \(x\), and let \(E\) be the set of \(x \in (0, 1]\) such that \(F(d_{n+1}(x), \dots, d_{n+m}(x)) \ge \Psi(n)\) for infinitely many \(n\). If \(\sum_{n \ge 0} G(\Psi(n)) < \infty\) then \(E\) has Lebesgue measure \(0\), and if \(\sum_{n \ge 0} G(M \Psi(n)) = \infty\) then \(E\) has Lebesgue measure \(1\).

Here \(M\) is any constant with this property (the paper takes the supremum; a larger \(M\) only weakens the divergence condition). Unlike the paper, \(\Psi\) need not be positive.

public theorem_wanted volume_lurothConsecutiveDigits_zero_one_integral {m : ℕ}
    (F : (Fin m → ℝ) → ℝ) (hFm : Measurable F)
    (hpos : ∀ x : Fin m → ℝ, (∀ i, 2 ≤ x i) → 0 < F x)
    (hmono : MonotoneOn F {x | ∀ i, 2 ≤ x i}) (M : ℝ)
    (hM : ∀ x : Fin m → ℝ, (∀ i, 2 ≤ x i) → F x ≤ M * F (fun i => (⌊x i⌋₊ : ℝ)))
    (Ψ : ℕ → ℝ) :
    let G : ℝ → ℝ≥0∞ := fun y =>
      ∫⁻ x in {x : Fin m → ℝ | (∀ i, 2 ≤ x i) ∧ y ≤ F x}, ENNReal.ofReal (∏ i, 1 / x i ^ 2)
    let E := {x ∈ Set.Ioc (0 : ℝ) 1 |
      ∃ᶠ n in atTop, Ψ n ≤ F (fun i => (lurothDigitSeq x (n + i) : ℝ))}
    (∑' n, G (Ψ n) < ∞ → volume E = 0) ∧ (∑' n, G (M * Ψ n) = ∞ → volume E = 1)

Sources

• Dmitry Kleinbock and Yuqing Zhang, Metrical Properties of Functions of Consecutive Digits in Lüroth Series, INTEGERS 24 (2024), Article A67, Theorem 4, with (6) and G from (7).

Uses 1

Statement usesLüroth digits

TheoremBorel–Cantelli dichotomy for Lüroth cylinder events#●ready to prove

Let \(m \in \mathbb{N}\), let \((S_n)_{n \ge 0}\) be a sequence of sets of \(m\)-tuples of natural numbers, write \(d_k(x)\) for the \(k\)-th Lüroth digit of \(x\) and \(\lambda\) for Lebesgue measure. Put \(A_n = \{x \in (0, 1] : (d_1(x), \dots, d_m(x)) \in S_n\}\) (a union of cylinders of level \(m\)) and let \(E\) be the set of \(x \in (0, 1]\) such that \((d_{n+1}(x), \dots, d_{n+m}(x)) \in S_n\) for infinitely many \(n\). If \(\sum_{n \ge 0} \lambda(A_n) < \infty\) then \(\lambda(E) = 0\), and if \(\sum_{n \ge 0} \lambda(A_n) = \infty\) then \(\lambda(E) = 1\).

public theorem_wanted volume_limsup_lurothPreimage_zero_one {m : ℕ}
    (S : ℕ → Set (Fin m → ℕ)) :
    let A : ℕ → Set ℝ := fun n =>
      {x ∈ Set.Ioc (0 : ℝ) 1 | (fun i : Fin m => lurothDigitSeq x i) ∈ S n}
    let E := {x ∈ Set.Ioc (0 : ℝ) 1 |
      ∃ᶠ n in atTop, (fun i : Fin m => lurothDigitSeq x (n + i)) ∈ S n}
    (∑' n, volume (A n) < ∞ → volume E = 0) ∧ (∑' n, volume (A n) = ∞ → volume E = 1)

Sources

• Dmitry Kleinbock and Yuqing Zhang, Metrical Properties of Functions of Consecutive Digits in Lüroth Series, INTEGERS 24 (2024), Article A67, Theorem 5.

Uses 1

Statement usesLüroth digits

TheoremUpper bound for the measure of a Lüroth digit superlevel set#●ready to prove

Let \(m \in \mathbb{N}\), let \(F : \mathbb{R}^m \to \mathbb{R}\) be non-decreasing on \([2, \infty)^m\) for the coordinatewise order, let \(y \in \mathbb{R}\), and write \(d_k(x)\) for the \(k\)-th Lüroth digit of \(x\). Then the Lebesgue measure of \(\{x \in (0, 1] : F(d_1(x), \dots, d_m(x)) \ge y\}\) is at most

\[3^m \int_{\{x \in [2, \infty)^m : F(x) \ge y\}} \prod_{i=1}^{m} \frac{1}{x_i^2} \, dx.\]

The paper states this bound for \(y = \Psi(n)\) under the hypotheses of its Theorem 4; only the monotonicity of \(F\) is used.

public theorem_wanted volume_lurothDigits_ge_le {m : ℕ} (F : (Fin m → ℝ) → ℝ)
    (hmono : MonotoneOn F {x | ∀ i, 2 ≤ x i}) (y : ℝ) :
    volume {x ∈ Set.Ioc (0 : ℝ) 1 | y ≤ F (fun i => (lurothDigitSeq x i : ℝ))} ≤
      3 ^ m * ∫⁻ x in {x : Fin m → ℝ | (∀ i, 2 ≤ x i) ∧ y ≤ F x},
        ENNReal.ofReal (∏ i, 1 / x i ^ 2)

Sources

• Dmitry Kleinbock and Yuqing Zhang, Metrical Properties of Functions of Consecutive Digits in Lüroth Series, INTEGERS 24 (2024), Article A67, Theorem 6.

Uses 1

Statement usesLüroth digits

TheoremLower bound for the measure of large Lüroth digit values#●ready to prove

Let \(m\) be a natural number, let \(D = [2, \infty)^m\), let \(F : \mathbb{R}^m \to \mathbb{R}\) satisfy \(F(x) > 0\) for every \(x \in D\), and let \(M\) be a real number with \(F(x) \le M\,F(\lfloor x_1 \rfloor, \ldots, \lfloor x_m \rfloor)\) for every \(x \in D\) (the paper's condition (6)). Put \(G(y) = \int_{\{x \in D \,:\, F(x) \ge y\}} \prod_{i=1}^m x_i^{-2}\,dx\) for real \(y\), let \(\lambda\) be Lebesgue measure on \(\mathbb{R}\) and let \(d_1(x), d_2(x), \ldots\) be the Lüroth digits of \(x\). Then for every real \(y\),

\[G(My) \le \lambda\{x \in (0, 1] : F(d_1(x), \ldots, d_m(x)) \ge y\}.\]

The paper states it only at the values of the sequence in its Theorem 4, under that theorem's hypotheses, which also require \(F\) to be measurable and non-decreasing; only positivity and condition (6) are assumed here.

public theorem_wanted le_volume_lurothDigits_ge {m : ℕ} (F : (Fin m → ℝ) → ℝ)
    (hpos : ∀ x : Fin m → ℝ, (∀ i, 2 ≤ x i) → 0 < F x) (M : ℝ)
    (hM : ∀ x : Fin m → ℝ, (∀ i, 2 ≤ x i) → F x ≤ M * F (fun i => (⌊x i⌋₊ : ℝ))) (y : ℝ) :
    (∫⁻ x in {x : Fin m → ℝ | (∀ i, 2 ≤ x i) ∧ M * y ≤ F x},
        ENNReal.ofReal (∏ i, 1 / x i ^ 2)) ≤
      volume {x ∈ Set.Ioc (0 : ℝ) 1 | y ≤ F (fun i => (lurothDigitSeq x i : ℝ))}

Sources

• Dmitry Kleinbock and Yuqing Zhang, Metrical Properties of Functions of Consecutive Digits in Lüroth Series, INTEGERS 24 (2024), Article A67, Theorem 7.

Uses 1

Statement usesLüroth digits

DefinitionWell approximable numbers#✓fully proved

For a function \(\psi : \mathbb{N} \to \mathbb{R}\), the set \(W(\psi)\) of \(\psi\)-well approximable numbers consists of the real numbers \(x \in [0, 1)\) such that for infinitely many natural numbers \(q\) there is an integer \(p\) with \(|x - p/q| < \psi(q)/q\).

The fractions \(p/q\) need not be in lowest terms, unlike Mathlib's well approximable sets, which use points of exact additive order \(q\). The value \(\psi(0)\) is irrelevant.

public def wellApproximableSet (ψ : ℕ → ℝ) : Set ℝ :=
  {x | x ∈ Set.Ico 0 1 ∧ ∃ᶠ q : ℕ in atTop, ∃ p : ℤ, |x - p / q| < ψ q / q}

Sources

• Ying Wai Lee, Lüroth Expansions in Diophantine Approximation: Metric Properties and Conjectures, INTEGERS 26 (2026), Article A45, equation (1).

Used by 4

Used byDodson's theorem · Jarník–Besicovitch theorem · Khintchine's theorem · Well approximable numbers lie in \((0, 1)\)

TheoremWell approximable numbers lie in \((0, 1)\)#✓fully proved

For every function \(\psi : \mathbb{N} \to \mathbb{R}\), every point of the set \(W(\psi)\) of \(\psi\)-well approximable numbers lies in the interval \([0, 1)\).

public theorem wellApproximableSet_subset_Ico (ψ : ℕ → ℝ) :
    wellApproximableSet ψ ⊆ Set.Ico 0 1

Sources

• Ying Wai Lee, Lüroth Expansions in Diophantine Approximation: Metric Properties and Conjectures, INTEGERS 26 (2026), Article A45, equation (1).

Uses 1

Statement usesWell approximable numbers

DefinitionLower order at infinity#✓fully proved

For \(\psi : \mathbb{N} \to \mathbb{R}\), the lower order at infinity of \(1/\psi\) is

\[\tau_\psi = \liminf_{q \to \infty} \max\left(-\frac{\log \psi(q)}{\log q},\, 0\right),\]

with the liminf taken in \([0, \infty]\). Here \(\log x\) means \(\log |x|\) for \(x \ne 0\) and \(\log 0 = 0\), and the ratio is read as \(0\) when \(\log q = 0\). For \(\psi\) with values in \((0, 1]\) the ratio is nonnegative once \(q \ge 2\), so the truncation at \(0\) has no effect there, and \(\tau_\psi\) may be infinite.

public noncomputable def lowerOrderAtInfinity (ψ : ℕ → ℝ) : ℝ≥0∞ :=
  liminf (fun q : ℕ => ENNReal.ofReal (-Real.log (ψ q) / Real.log q)) atTop

Sources

• Ying Wai Lee, Lüroth Expansions in Diophantine Approximation: Metric Properties and Conjectures, INTEGERS 26 (2026), Article A45, equation (11).

Used by 7

Used byDimension bounds for Lüroth well approximable sets · Dimension bounds for Lüroth well approximable sets via denominators · Dimension of Lüroth well approximable sets under a divergence condition · Dodson's theorem · Without monotonicity the Lüroth dimension can vanish · Lower order at infinity of a power function · Lüroth well approximable numbers as a limsup over convergent triples

DefinitionUpper order at infinity#✓fully proved

For a function \(\psi\) from the natural numbers to the reals, the upper order at infinity of \(\psi\) is the element

\[\bar\tau_\psi = \limsup_{q \to \infty} \max\left(0, \frac{-\log \psi(q)}{\log q}\right)\]

of \([0, \infty]\).

public noncomputable def upperOrderAtInfinity (ψ : ℕ → ℝ) : ℝ≥0∞ :=
  limsup (fun q : ℕ => ENNReal.ofReal (-Real.log (ψ q) / Real.log q)) atTop

Sources

• Ying Wai Lee, Lüroth Expansions in Diophantine Approximation: Metric Properties and Conjectures, INTEGERS 26 (2026), Article A45, equation (11).

Used by 3

Used byDimension bounds for Lüroth well approximable sets · Dimension bounds for Lüroth well approximable sets via denominators · Upper order at infinity of \(q^{-\tau}\)

TheoremThe order ratio of \(q^{-\tau}\)#✓fully proved

For every real \(\tau\) and all sufficiently large natural numbers \(q\), \(\max(0, -\log((q^{\tau})^{-1})/\log q) = \max(0, \tau)\).

public theorem orderRatio_rpow_inv (τ : ℝ) :
    ∀ᶠ q : ℕ in atTop,
      ENNReal.ofReal (-Real.log (((q : ℝ) ^ τ)⁻¹) / Real.log q) = ENNReal.ofReal τ

Sources

• Ying Wai Lee, Lüroth Expansions in Diophantine Approximation: Metric Properties and Conjectures, INTEGERS 26 (2026), Article A45, equation (11).

Used by 2

Used byLower order at infinity of a power function · Upper order at infinity of \(q^{-\tau}\)

TheoremLower order at infinity of a power function#✓fully proved

For a real number \(\tau\), let \(\psi : \mathbb{N} \to \mathbb{R}\) be given by \(\psi(q) = q^{-\tau}\) (the value at \(q = 0\) does not matter). Then the lower order at infinity of \(1/\psi\) is \(\tau_\psi = \max(\tau, 0)\), an element of \([0, \infty]\); in particular \(\tau_\psi = \tau\) when \(\tau \ge 0\).

public theorem lowerOrderAtInfinity_rpow_inv (τ : ℝ) :
    lowerOrderAtInfinity (fun q => ((q : ℝ) ^ τ)⁻¹) = ENNReal.ofReal τ

Sources

• Ying Wai Lee, Lüroth Expansions in Diophantine Approximation: Metric Properties and Conjectures, INTEGERS 26 (2026), Article A45, remark after Theorem 7.

Uses 2

Statement usesLower order at infinity

Proof usesThe order ratio of \(q^{-\tau}\)

TheoremUpper order at infinity of \(q^{-\tau}\)#✓fully proved

For every real \(\tau\), the upper order at infinity of \(q \mapsto (q^{\tau})^{-1}\) is \(\max(0, \tau)\); in particular it is \(\tau\) when \(\tau \ge 0\).

public theorem upperOrderAtInfinity_rpow_inv (τ : ℝ) :
    upperOrderAtInfinity (fun q => ((q : ℝ) ^ τ)⁻¹) = ENNReal.ofReal τ

Sources

• Ying Wai Lee, Lüroth Expansions in Diophantine Approximation: Metric Properties and Conjectures, INTEGERS 26 (2026), Article A45, remark after Theorem 7.

Uses 2

Statement usesUpper order at infinity

Proof usesThe order ratio of \(q^{-\tau}\)

TheoremKhintchine's theorem#●ready to prove

Let \(\psi : \mathbb{N} \to \mathbb{R}\) be non-increasing on all of \(\mathbb{N}\) (including \(\psi(0) \ge \psi(1)\)) with \(0 \le \psi(q) \le 1/2\) for every \(q\). If the series \(\sum_q \psi(q)\) converges, then the set \(W(\psi)\) of \(\psi\)-well approximable numbers has Lebesgue measure \(0\); if the series diverges, then \(W(\psi)\) has Lebesgue measure \(1\).

The value \(\psi(0)\) affects neither \(W(\psi)\) nor the convergence of the series, so the condition at \(0\) costs nothing: extend by \(\psi(0) = \psi(1)\).

public theorem_wanted volume_wellApproximableSet_khintchine (ψ : ℕ → ℝ)
    (hψ0 : ∀ q, 0 ≤ ψ q) (hψ1 : ∀ q, ψ q ≤ 1 / 2) (hψ : Antitone ψ) :
    (Summable ψ → volume (wellApproximableSet ψ) = 0) ∧
      (¬ Summable ψ → volume (wellApproximableSet ψ) = 1)

Sources

• Ying Wai Lee, Lüroth Expansions in Diophantine Approximation: Metric Properties and Conjectures, INTEGERS 26 (2026), Article A45, Theorem 1 (Khintchine).

Uses 1

Statement usesWell approximable numbers

TheoremJarník–Besicovitch theorem#●ready to prove

For a real number \(\tau \ge 1\), let \(W(\tau)\) be the set of \(x \in [0, 1)\) such that for infinitely many natural numbers \(q\) there is an integer \(p\) with \(|x - p/q| < q^{-(1+\tau)}\); this is the set of \(\psi\)-well approximable numbers for \(\psi(q) = q^{-\tau}\). Then the Hausdorff dimension of \(W(\tau)\) is \(2/(1 + \tau)\).

public theorem_wanted dimH_wellApproximableSet_rpow (τ : ℝ) (hτ : 1 ≤ τ) :
    dimH (wellApproximableSet (fun q => ((q : ℝ) ^ τ)⁻¹)) = ENNReal.ofReal (2 / (1 + τ))

Sources

• Ying Wai Lee, Lüroth Expansions in Diophantine Approximation: Metric Properties and Conjectures, INTEGERS 26 (2026), Article A45, Theorem 2 (Jarník; Besicovitch).

Uses 1

Statement usesWell approximable numbers

TheoremDodson's theorem#●ready to prove

Let \(\psi\) be a non-increasing function from the natural numbers to \((0, 1/2]\), let \(W(\psi)\) be the set of \(x \in [0, 1)\) such that for infinitely many \(q\) there is an integer \(p\) with \(|x - p/q| < \psi(q)/q\), and let \(\tau_\psi = \liminf_{q \to \infty} (-\log \psi(q) / \log q)\), taken in \([0, \infty]\), be the lower order at infinity of \(1/\psi\). If \(\tau_\psi \ge 1\), then the Hausdorff dimension of \(W(\psi)\) is \(2/(1 + \tau_\psi)\), read as \(0\) when \(\tau_\psi = \infty\).

The paper allows \(\psi(q) = 0\); here \(\psi\) is assumed positive, so that \(\log \psi(q)\) is defined. Without the hypothesis \(\tau_\psi \ge 1\) the formula fails: the constant \(\psi = 1/4\) has \(\tau_\psi = 0\) and \(\dim_H W(\psi) = 1\).

public theorem_wanted dimH_wellApproximableSet_dodson (ψ : ℕ → ℝ)
    (hψ0 : ∀ q, 0 < ψ q) (hψ1 : ∀ q, ψ q ≤ 1 / 2) (hψ : Antitone ψ)
    (hτ : 1 ≤ lowerOrderAtInfinity ψ) :
    dimH (wellApproximableSet ψ) = 2 * (1 + lowerOrderAtInfinity ψ)⁻¹

Sources

• Ying Wai Lee, Lüroth Expansions in Diophantine Approximation: Metric Properties and Conjectures, INTEGERS 26 (2026), Article A45, Theorem 3 (Dodson).

Uses 2

Statement usesLower order at infinity · Well approximable numbers

DefinitionLüroth denominators#✓fully proved

For a sequence of natural numbers \(d_0, d_1, d_2, \dots\) (numbered from \(0\)), the \(n\)-th Lüroth denominator is

\[Q_n = d_n \prod_{j=0}^{n-1} d_j (d_j - 1), \qquad n \ge 0.\]

With digits numbered from \(1\), as in the paper, this is the paper's \(Q_{n+1}\).

public def lurothDenominator (d : ℕ → ℕ) (n : ℕ) : ℕ :=
  d n * ∏ j ∈ Finset.range n, d j * (d j - 1)

Sources

• Ying Wai Lee, Lüroth Expansions in Diophantine Approximation: Metric Properties and Conjectures, INTEGERS 26 (2026), Article A45, equation (8).

Used by 10

Used byDimension bounds for Lüroth well approximable sets via denominators · A Lüroth triple from the expansion of \(1\) · Lüroth convergents · Lüroth convergents approximate from below · Recurrence for Lüroth convergents · Recurrence for Lüroth denominators · Lüroth denominators of the constant digit sequence 2 · Lüroth convergent triples · Lüroth well approximable numbers · Lüroth well approximable numbers lie in \((0, 1)\)

DefinitionLüroth convergents#✓fully proved

For a sequence of natural numbers \(d_0, d_1, d_2, \dots\) (numbered from \(0\)) with Lüroth denominators \(Q_0, Q_1, Q_2, \dots\), the \(n\)-th Lüroth convergent is the rational number

\[x_n = \sum_{k=0}^{n} \frac{1}{Q_k}, \qquad n \ge 0,\]

where a term with \(Q_k = 0\) is read as \(0\). With digits numbered from \(1\), as in the paper, this is the paper's \(x_{n+1} = P_{n+1}/Q_{n+1}\).

public def lurothConvergent (d : ℕ → ℕ) (n : ℕ) : ℚ :=
  ∑ k ∈ Finset.range (n + 1), 1 / (lurothDenominator d k : ℚ)

Sources

• Ying Wai Lee, Lüroth Expansions in Diophantine Approximation: Metric Properties and Conjectures, INTEGERS 26 (2026), Article A45, Section 2.

Uses 1 · Used by 7

Statement usesLüroth denominators

Used byRecognising Lüroth convergents · A Lüroth triple from the expansion of \(1\) · Lüroth convergents approximate from below · Recurrence for Lüroth convergents · Lüroth convergent triples · Lüroth well approximable numbers · Lüroth well approximable numbers lie in \((0, 1)\)

TheoremThe Lüroth digits of 1#✓fully proved

Every Lüroth digit of \(1\) equals \(2\), that is, \(1 = [2, 2, 2, \dots]\) in Lüroth notation.

public theorem lurothDigitSeq_one (n : ℕ) : lurothDigitSeq 1 n = 2

Sources

• Ying Wai Lee, Lüroth Expansions in Diophantine Approximation: Metric Properties and Conjectures, INTEGERS 26 (2026), Article A45, Section 2.

Uses 5 · Used by 1

Statement usesLüroth digits

Proof usesFirst Lüroth digit · First Lüroth digit of 1 · Lüroth map · The Lüroth map fixes 1

Used byA Lüroth triple from the expansion of \(1\)

TheoremThe Lüroth orbit of \(27/71\) has period two#✓fully proved

The Lüroth map \(T\) sends \(27/71\) to \(20/71\) and sends \(20/71\) to \(27/71\); in particular \(T(T(27/71)) = 27/71\).

public theorem lurothMap_lurothMap_27_71 :
    lurothMap (27 / 71) = 20 / 71 ∧ lurothMap (20 / 71) = 27 / 71

Sources

• Ying Wai Lee, Lüroth Expansions in Diophantine Approximation: Metric Properties and Conjectures, INTEGERS 26 (2026), Article A45, Section 2 (example).

Uses 2

Statement usesLüroth map

Proof usesFirst Lüroth digit

TheoremRecurrence for Lüroth denominators#✓fully proved

For every sequence of natural numbers \(d_0, d_1, d_2, \dots\) with Lüroth denominators \(Q_0, Q_1, Q_2, \dots\) and every \(n \ge 0\),

\[Q_{n+1} = Q_n (d_n - 1) d_{n+1}.\]

public theorem lurothDenominator_succ (d : ℕ → ℕ) (n : ℕ) :
    lurothDenominator d (n + 1) = lurothDenominator d n * (d n - 1) * d (n + 1)

Sources

• Ying Wai Lee, Lüroth Expansions in Diophantine Approximation: Metric Properties and Conjectures, INTEGERS 26 (2026), Article A45, equation (8).

Uses 1 · Used by 1

Statement usesLüroth denominators

Used byLüroth denominators of the constant digit sequence 2

TheoremLüroth denominators of the constant digit sequence 2#✓fully proved

If \(d_j = 2\) for every \(j \ge 0\), then the Lüroth denominators are \(Q_n = 2^{n+1}\) for every \(n \ge 0\) (digits numbered from \(0\); this is the paper's \(Q_{n+1} = 2^{n+1}\)).

public theorem lurothDenominator_two (n : ℕ) :
    lurothDenominator (fun _ => 2) n = 2 ^ (n + 1)

Sources

• Ying Wai Lee, Lüroth Expansions in Diophantine Approximation: Metric Properties and Conjectures, INTEGERS 26 (2026), Article A45, equation (8).

Uses 2

Statement usesLüroth denominators

Proof usesRecurrence for Lüroth denominators

TheoremRecurrence for Lüroth convergents#✓fully proved

For every sequence of natural numbers \(d_0, d_1, d_2, \dots\) with Lüroth denominators \(Q_n\) and Lüroth convergents \(x_n\), and every \(n \ge 0\), \(x_{n+1} = x_n + 1/Q_{n+1}\), where \(1/Q_{n+1}\) is read as \(0\) if \(Q_{n+1} = 0\).

public theorem lurothConvergent_succ (d : ℕ → ℕ) (n : ℕ) :
    lurothConvergent d (n + 1) =
      lurothConvergent d n + 1 / (lurothDenominator d (n + 1) : ℚ)

Sources

• Ying Wai Lee, Lüroth Expansions in Diophantine Approximation: Metric Properties and Conjectures, INTEGERS 26 (2026), Article A45, Section 2.

Uses 2

Statement usesLüroth convergents · Lüroth denominators

DefinitionLüroth well approximable numbers#✓fully proved

For a function \(\psi\) from the natural numbers to the reals, \(L(\psi)\) is the set of \(x \in (0, 1]\) such that \(|x - c_n(x)| < \psi(Q_n(x))/Q_n(x)\) for infinitely many \(n\), where \(Q_n(x)\) and \(c_n(x)\) are the \(n\)-th Lüroth denominator and the \(n\)-th Lüroth convergent of the Lüroth digit sequence of \(x\).

public def lurothWellApproximableSet (ψ : ℕ → ℝ) : Set ℝ :=
  {x | x ∈ Set.Ioc 0 1 ∧ ∃ᶠ n in atTop,
    |x - lurothConvergent (lurothDigitSeq x) n| <
      ψ (lurothDenominator (lurothDigitSeq x) n) / lurothDenominator (lurothDigitSeq x) n}

Sources

• Ying Wai Lee, Lüroth Expansions in Diophantine Approximation: Metric Properties and Conjectures, INTEGERS 26 (2026), Article A45, Section 2.

Uses 3 · Used by 10

Statement usesLüroth convergents · Lüroth denominators · Lüroth digits

Used byHausdorff dimension and measure of Lüroth well approximable sets for powers · Dimension bounds for Lüroth well approximable sets · Dimension bounds for Lüroth well approximable sets via denominators · Dimension of Lüroth well approximable sets under a divergence condition · Cao–Wu–Zhang theorem · Without monotonicity the Lüroth dimension can vanish · Lüroth well approximable numbers as a limsup over convergent triples · Lüroth \(q^{-\tau}\)-well approximable numbers as a limsup over convergent triples · Lüroth well approximable numbers lie in \((0, 1)\) · Tan–Zhou theorem (Lüroth analogue of Khintchine's theorem)

TheoremLüroth well approximable numbers lie in \((0, 1)\)#✓fully proved

For every function \(\psi\) from the natural numbers to the reals, the set \(L(\psi)\) of Lüroth \(\psi\)-well approximable numbers is contained in \((0, 1]\).

public theorem lurothWellApproximableSet_subset_Ioc (ψ : ℕ → ℝ) :
    lurothWellApproximableSet ψ ⊆ Set.Ioc 0 1

Sources

• Ying Wai Lee, Lüroth Expansions in Diophantine Approximation: Metric Properties and Conjectures, INTEGERS 26 (2026), Article A45, Section 2.

Uses 4

Statement usesLüroth well approximable numbers

Proof usesLüroth convergents · Lüroth denominators · Lüroth digits

DefinitionLüroth convergent triples#✓fully proved

The set \(S\) consists of the triples \((c_n(y), Q_n(y), d_n(y))\) for \(y \in (0, 1]\) and \(n \ge 0\), where \(d_0(y), d_1(y), \dots\) are the Lüroth digits of \(y\) (indexed from \(0\)), \(Q_n(y) = d_n(y) \prod_{j < n} d_j(y)(d_j(y) - 1)\) is the \(n\)-th Lüroth denominator of this digit sequence, and \(c_n(y) = \sum_{k \le n} 1/Q_k(y)\) is its \(n\)-th Lüroth convergent. The first entry is the rational number \(c_n(y)\), the second the natural number \(Q_n(y)\) and the third the digit \(d_n(y)\).

public def lurothTripleSet : Set (ℚ × ℕ × ℕ) :=
  {t | ∃ y ∈ Set.Ioc (0 : ℝ) 1, ∃ n,
    t = (lurothConvergent (lurothDigitSeq y) n, lurothDenominator (lurothDigitSeq y) n,
      lurothDigitSeq y n)}

Sources

• Ying Wai Lee, Lüroth Expansions in Diophantine Approximation: Metric Properties and Conjectures, INTEGERS 26 (2026), Article A45, equation (16).

Uses 3 · Used by 4

Statement usesLüroth convergents · Lüroth denominators · Lüroth digits

Used byRecognising Lüroth convergents · A Lüroth triple from the expansion of \(1\) · Lüroth well approximable numbers as a limsup over convergent triples · Lüroth \(q^{-\tau}\)-well approximable numbers as a limsup over convergent triples

TheoremA Lüroth triple from the expansion of \(1\)#✓fully proved

Let \(S\) be the set of triples \((P_n(y)/Q_n(y), Q_n(y), d_n(y))\) for \(y \in (0, 1]\) and \(n \ge 0\), where \(P_n(y)/Q_n(y)\) is the \(n\)-th Lüroth convergent of \(y\), \(Q_n(y)\) its Lüroth denominator and \(d_n(y)\) its \(n\)-th Lüroth digit (indexed from \(0\)). Then \((1/2, 2, 2) \in S\): it is the triple of the first convergent of \(1 = [2, 2, 2, \ldots]\).

public theorem half_two_two_mem_lurothTripleSet : ((1 / 2 : ℚ), 2, 2) ∈ lurothTripleSet

Sources

• Ying Wai Lee, Lüroth Expansions in Diophantine Approximation: Metric Properties and Conjectures, INTEGERS 26 (2026), Article A45, equation (16).

Uses 5

Statement usesLüroth convergent triples

Proof usesLüroth convergents · Lüroth denominators · Lüroth digits · The Lüroth digits of 1

TheoremLüroth convergents approximate from below#●ready to prove

Let \(x \in (0, 1]\) have Lüroth digits \(d_0, d_1, d_2, \dots\) (numbered from \(0\)), Lüroth denominators \(Q_0, Q_1, Q_2, \dots\) and Lüroth convergents \(x_0, x_1, x_2, \dots\). Then for every \(n \ge 0\),

\[0 < x - x_n \le \frac{1}{(d_n - 1) Q_n}.\]

In the paper's numbering from \(1\) these are \(d_{n+1}\), \(Q_{n+1}\) and \(x_{n+1} = P_{n+1}/Q_{n+1}\).

public theorem_wanted lurothConvergent_lt_le (x : ℝ) (hx : x ∈ Set.Ioc 0 1) (n : ℕ) :
    0 < x - lurothConvergent (lurothDigitSeq x) n ∧
      x - lurothConvergent (lurothDigitSeq x) n ≤
        1 / (((lurothDigitSeq x n : ℝ) - 1) * lurothDenominator (lurothDigitSeq x) n)

Sources

• Ying Wai Lee, Lüroth Expansions in Diophantine Approximation: Metric Properties and Conjectures, INTEGERS 26 (2026), Article A45, Proposition 1.

Uses 3

Statement usesLüroth convergents · Lüroth denominators · Lüroth digits

TheoremMass transference principle for intervals#●ready to prove

Let \((c_n)\) and \((r_n)\) be real sequences with \(r_n \ge 0\) for every \(n\) and \(r_n \to 0\), and let \(I_n = [c_n - r_n, c_n + r_n]\). Assume that \(I_n \subseteq [0, 1]\) for every \(n\), let \(0 < s < 1\), and let \(I_n^s = [c_n - r_n^s, c_n + r_n^s]\). If \([0, 1] \cap \limsup_{n \to \infty} I_n^s\) has Lebesgue measure \(1\), then the \(s\)-dimensional Hausdorff measure of \(\limsup_{n \to \infty} I_n\) is infinite and the Hausdorff dimension of \(\limsup_{n \to \infty} I_n\) is at least \(s\).

The endpoints \(s = 0\) and \(s = 1\) admitted by the printed statement are excluded. For \(s = 0\), the intervals \(I_n = [1/2 - 1/(n+2), 1/2 + 1/(n+2)]\) satisfy the hypothesis, but \(\limsup I_n\) is the single point \(1/2\), whose \(0\)-dimensional Hausdorff measure is \(1\). For \(s = 1\), the \(1\)-dimensional Hausdorff measure of a subset of \([0, 1]\) is at most \(1\). The paper's proof treats \(0 < s < 1\).

public theorem_wanted hausdorffMeasure_limsup_closedBall_of_volume (c r : ℕ → ℝ) (s : ℝ)
    (hs0 : 0 < s) (hs1 : s < 1) (hr0 : ∀ n, 0 ≤ r n)
    (hI : ∀ n, Metric.closedBall (c n) (r n) ⊆ Set.Icc 0 1)
    (hr : Tendsto r atTop (nhds 0))
    (hfull : volume (Set.Icc 0 1 ∩
      limsup (fun n => Metric.closedBall (c n) (r n ^ s)) atTop) = 1) :
    μH[s] (limsup (fun n => Metric.closedBall (c n) (r n)) atTop) = ∞ ∧
      ENNReal.ofReal s ≤ dimH (limsup (fun n => Metric.closedBall (c n) (r n)) atTop)

Sources

• Ying Wai Lee, Lüroth Expansions in Diophantine Approximation: Metric Properties and Conjectures, INTEGERS 26 (2026), Article A45, Proposition 3.

TheoremRecognising Lüroth convergents#●ready to prove

For \(y \in (0, 1]\) and \(n \ge 0\) let \(P_n(y)/Q_n(y)\) be the \(n\)-th Lüroth convergent of \(y\), \(Q_n(y)\) its Lüroth denominator and \(d_n(y)\) the \(n\)-th Lüroth digit of \(y\), and let \(S\) be the set of all triples \((P_n(y)/Q_n(y), Q_n(y), d_n(y))\) for \(y \in (0, 1]\) and \(n \ge 0\). If \(x \in (0, 1]\) and \((P/Q, Q, d) \in S\) satisfy \(0 < x - P/Q \le 1/((d - 1) Q)\), then \(P/Q\) is a Lüroth convergent of \(x\), that is, \(P/Q = P_n(x)/Q_n(x)\) for some \(n\).

public theorem_wanted exists_lurothConvergent_eq_of_mem_lurothTripleSet (x : ℝ)
    (hx : x ∈ Set.Ioc 0 1) (t : ℚ × ℕ × ℕ) (ht : t ∈ lurothTripleSet)
    (hpos : 0 < x - t.1) (hle : x - t.1 ≤ 1 / (((t.2.2 : ℝ) - 1) * t.2.1)) :
    ∃ n, lurothConvergent (lurothDigitSeq x) n = t.1

Sources

• Ying Wai Lee, Lüroth Expansions in Diophantine Approximation: Metric Properties and Conjectures, INTEGERS 26 (2026), Article A45, Proposition 4.

Uses 3

Statement usesLüroth convergents · Lüroth digits · Lüroth convergent triples

TheoremLüroth \(q^{-\tau}\)-well approximable numbers as a limsup over convergent triples#●ready to prove

Let \(\tau \ge 0\) and let \(L(\tau)\) be the set of Lüroth \(\psi\)-well approximable numbers for \(\psi(q) = q^{-\tau}\). For a triple \(t = (c, Q, d)\) in the set \(S\) of Lüroth convergent triples, put \(B_t = (c, c + Q^{-(1+\tau)}) \cap (c, c + 1/((d - 1)Q)]\). Then \(L(\tau)\) consists of the real numbers \(x\) that lie in \(B_t\) for infinitely many \(t \in S\).

public theorem_wanted lurothWellApproximableSet_rpow_eq_limsup (τ : ℝ) (hτ : 0 ≤ τ) :
    lurothWellApproximableSet (fun q => ((q : ℝ) ^ τ)⁻¹) =
      {x | {t ∈ lurothTripleSet |
        x ∈ Set.Ioo (t.1 : ℝ) (t.1 + ((t.2.1 : ℝ) ^ (1 + τ))⁻¹) ∩
          Set.Ioc (t.1 : ℝ) (t.1 + (((t.2.2 : ℝ) - 1) * t.2.1)⁻¹)}.Infinite}

Sources

• Ying Wai Lee, Lüroth Expansions in Diophantine Approximation: Metric Properties and Conjectures, INTEGERS 26 (2026), Article A45, Proposition 5.

Uses 2

Statement usesLüroth convergent triples · Lüroth well approximable numbers

TheoremLüroth well approximable numbers as a limsup over convergent triples#●ready to prove

Let \(\psi\) be a function from the natural numbers to \((0, 1]\) whose lower order at infinity \(\tau_\psi\) is greater than \(1\). Then the set \(L(\psi)\) of Lüroth \(\psi\)-well approximable numbers consists of the real numbers \(x\) for which there are infinitely many triples \((c, Q, d)\) in the set \(S\) of Lüroth convergent triples with \(c < x < c + \psi(Q)/Q\).

public theorem_wanted lurothWellApproximableSet_eq_limsup (ψ : ℕ → ℝ)
    (hψ0 : ∀ q, 0 < ψ q) (hψ1 : ∀ q, ψ q ≤ 1) (hτ : 1 < lowerOrderAtInfinity ψ) :
    lurothWellApproximableSet ψ =
      {x | {t ∈ lurothTripleSet |
        x ∈ Set.Ioo (t.1 : ℝ) (t.1 + ψ t.2.1 / t.2.1)}.Infinite}

Sources

• Ying Wai Lee, Lüroth Expansions in Diophantine Approximation: Metric Properties and Conjectures, INTEGERS 26 (2026), Article A45, Proposition 7.

Uses 3

Statement usesLower order at infinity · Lüroth convergent triples · Lüroth well approximable numbers

TheoremTan–Zhou theorem (Lüroth analogue of Khintchine's theorem)#●ready to prove

Let \(\psi\) be a non-increasing function from the natural numbers (including \(0\)) to \((0, 1]\), and let \(L(\psi)\) be the set of Lüroth \(\psi\)-well approximable numbers. If the series \(\sum_{q \ge 1} -\psi(q) \log \psi(q) / q\) converges, then \(L(\psi)\) has Lebesgue measure \(0\); if it diverges, then \(L(\psi)\) has Lebesgue measure \(1\).

public theorem_wanted volume_lurothWellApproximableSet (ψ : ℕ → ℝ)
    (hψ0 : ∀ q, 0 < ψ q) (hψ1 : ∀ q, ψ q ≤ 1) (hψ : Antitone ψ) :
    (Summable (fun q : ℕ => -ψ q * Real.log (ψ q) / q) →
        volume (lurothWellApproximableSet ψ) = 0) ∧
      (¬ Summable (fun q : ℕ => -ψ q * Real.log (ψ q) / q) →
        volume (lurothWellApproximableSet ψ) = 1)

Sources

• Ying Wai Lee, Lüroth Expansions in Diophantine Approximation: Metric Properties and Conjectures, INTEGERS 26 (2026), Article A45, Theorem 4 (Tan and Zhou).

Uses 1

Statement usesLüroth well approximable numbers

TheoremCao–Wu–Zhang theorem#●ready to prove

For \(x \in (0, 1]\) let \(P_n(x)/Q_n(x)\) be the \(n\)-th Lüroth convergent of \(x\), with Lüroth denominator \(Q_n(x)\). For a real number \(\tau \ge 1\) let \(L(\tau)\) be the set of \(x \in (0, 1]\) such that \(|x - P_n(x)/Q_n(x)| < Q_n(x)^{-\tau}/Q_n(x)\) for infinitely many \(n\), that is, the set of Lüroth \(\psi\)-well approximable numbers for \(\psi(q) = q^{-\tau}\). Then the Hausdorff dimension of \(L(\tau)\) is \(1/(1 + \tau)\).

public theorem_wanted dimH_lurothWellApproximableSet_rpow_of_one_le (τ : ℝ) (hτ : 1 ≤ τ) :
    dimH (lurothWellApproximableSet (fun q => ((q : ℝ) ^ τ)⁻¹)) =
      ENNReal.ofReal (1 / (1 + τ))

Sources

• Ying Wai Lee, Lüroth Expansions in Diophantine Approximation: Metric Properties and Conjectures, INTEGERS 26 (2026), Article A45, Theorem 5 (Cao, Wu, and Zhang).

Uses 1

Statement usesLüroth well approximable numbers

TheoremHausdorff dimension and measure of Lüroth well approximable sets for powers#●ready to prove

For \(x \in (0, 1]\) let \(P_n(x)/Q_n(x)\) be the \(n\)-th Lüroth convergent of \(x\), with Lüroth denominator \(Q_n(x)\). For a real number \(\tau \ge 0\) let \(L(\tau)\) be the set of \(x \in (0, 1]\) such that \(|x - P_n(x)/Q_n(x)| < Q_n(x)^{-\tau}/Q_n(x)\) for infinitely many \(n\), that is, the set of Lüroth \(\psi\)-well approximable numbers for \(\psi(q) = q^{-\tau}\). Then the Hausdorff dimension of \(L(\tau)\) is \(1/(1 + \tau)\), and if \(\tau > 0\), the \(1/(1 + \tau)\)-dimensional Hausdorff measure of \(L(\tau)\) is infinite.

The source also states the measure claim at \(\tau = 0\), where it fails: \(L(0)\) is contained in \((0, 1]\), so its \(1\)-dimensional Hausdorff measure is at most \(1\).

public theorem_wanted dimH_hausdorffMeasure_lurothWellApproximableSet_rpow (τ : ℝ)
    (hτ : 0 ≤ τ) :
    dimH (lurothWellApproximableSet (fun q => ((q : ℝ) ^ τ)⁻¹)) =
        ENNReal.ofReal (1 / (1 + τ)) ∧
      (0 < τ → μH[1 / (1 + τ)] (lurothWellApproximableSet (fun q => ((q : ℝ) ^ τ)⁻¹)) = ∞)

Sources

• Ying Wai Lee, Lüroth Expansions in Diophantine Approximation: Metric Properties and Conjectures, INTEGERS 26 (2026), Article A45, Theorem 6.

Uses 1

Statement usesLüroth well approximable numbers

TheoremDimension bounds for Lüroth well approximable sets#●ready to prove

Let \(\psi\) be a function from the natural numbers to \((0, 1]\). Let \(L(\psi)\) be the set of \(x \in (0, 1]\) such that \(|x - P_n(x)/Q_n(x)| < \psi(Q_n(x))/Q_n(x)\) for infinitely many \(n\), where \(P_n(x)/Q_n(x)\) is the \(n\)-th Lüroth convergent of \(x\) and \(Q_n(x)\) its Lüroth denominator. Let \(\tau_\psi = \liminf_{q \to \infty} (-\log \psi(q) / \log q)\) and \(\bar\tau_\psi = \limsup_{q \to \infty} (-\log \psi(q) / \log q)\), taken in \([0, \infty]\), be the lower and upper orders at infinity of \(1/\psi\). Then \(1/(1 + \bar\tau_\psi) \le \dim_H L(\psi) \le 1/(1 + \tau_\psi)\), where \(1/\infty = 0\).

public theorem_wanted dimH_lurothWellApproximableSet_bounds (ψ : ℕ → ℝ)
    (hψ0 : ∀ q, 0 < ψ q) (hψ1 : ∀ q, ψ q ≤ 1) :
    (1 + upperOrderAtInfinity ψ)⁻¹ ≤ dimH (lurothWellApproximableSet ψ) ∧
      dimH (lurothWellApproximableSet ψ) ≤ (1 + lowerOrderAtInfinity ψ)⁻¹

Sources

• Ying Wai Lee, Lüroth Expansions in Diophantine Approximation: Metric Properties and Conjectures, INTEGERS 26 (2026), Article A45, Theorem 7.

Uses 3

Statement usesLower order at infinity · Lüroth well approximable numbers · Upper order at infinity

TheoremDimension bounds for Lüroth well approximable sets via denominators#●ready to prove

Let \(\psi\) be a function from the natural numbers to \((0, 1]\). Let \(L(\psi)\) be the set of \(x \in (0, 1]\) such that \(|x - P_n(x)/Q_n(x)| < \psi(Q_n(x))/Q_n(x)\) for infinitely many \(n\), where \(P_n(x)/Q_n(x)\) is the \(n\)-th Lüroth convergent of \(x\) and \(Q_n(x)\) its Lüroth denominator. For \(k \ge 0\) let \(S_k\) be the set of numbers \(d_k \prod_{j < k} d_j (d_j - 1)\), where \(d_0, \ldots, d_k\) are integers at least \(2\) (the \(k\)-th Lüroth denominators, indexed from \(0\)). For \(q \ge 2\) put \(r(q) = -\log \psi(q) / \log q\), and let \(\lambda_\psi = \liminf_{k \to \infty} \liminf_{q \in S_k, q \to \infty} r(q)\), \(\bar\lambda_\psi = \liminf_{k \to \infty} \limsup_{q \in S_k, q \to \infty} r(q)\), \(\tau_\psi = \liminf_{q \to \infty} r(q)\) and \(\bar\tau_\psi = \limsup_{q \to \infty} r(q)\), all taken in \([0, \infty]\). Then \(\tau_\psi \le \lambda_\psi\), \(\bar\lambda_\psi \le \bar\tau_\psi\) and \(1/(1 + \bar\lambda_\psi) \le \dim_H L(\psi) \le 1/(1 + \lambda_\psi)\), where \(1/\infty = 0\).

Since \(S_k\) is indexed from \(0\), it is the paper's \(S_{k+1}\); this does not change the outer limit inferior.

public theorem_wanted dimH_lurothWellApproximableSet_bounds_denominators (ψ : ℕ → ℝ)
    (hψ0 : ∀ q, 0 < ψ q) (hψ1 : ∀ q, ψ q ≤ 1) :
    let S : ℕ → Set ℕ := fun k =>
      {q | ∃ d : ℕ → ℕ, (∀ n, 2 ≤ d n) ∧ lurothDenominator d k = q}
    let f : ℕ → ℝ≥0∞ := fun q => ENNReal.ofReal (-Real.log (ψ q) / Real.log q)
    let lowerLam : ℝ≥0∞ := liminf (fun k => liminf f (atTop ⊓ Filter.principal (S k))) atTop
    let upperLam : ℝ≥0∞ := liminf (fun k => limsup f (atTop ⊓ Filter.principal (S k))) atTop
    lowerOrderAtInfinity ψ ≤ lowerLam ∧ upperLam ≤ upperOrderAtInfinity ψ ∧
      (1 + upperLam)⁻¹ ≤ dimH (lurothWellApproximableSet ψ) ∧
      dimH (lurothWellApproximableSet ψ) ≤ (1 + lowerLam)⁻¹

Sources

• Ying Wai Lee, Lüroth Expansions in Diophantine Approximation: Metric Properties and Conjectures, INTEGERS 26 (2026), Article A45, Theorem 8.

Uses 4

Statement usesLower order at infinity · Lüroth denominators · Lüroth well approximable numbers · Upper order at infinity

TheoremWithout monotonicity the Lüroth dimension can vanish#●ready to prove

For every real number \(\tau \ge 0\) there is a function \(\psi\) from the natural numbers to \((0, 1]\) such that: \(\psi\) is not non-increasing on \(\{q : q \ge N\}\) for any \(N\); the lower order at infinity \(\liminf_{q \to \infty} (-\log \psi(q) / \log q)\) of \(1/\psi\) equals \(\tau\); and the set \(L(\psi)\) of \(x \in (0, 1]\) such that \(|x - P_n(x)/Q_n(x)| < \psi(Q_n(x))/Q_n(x)\) for infinitely many \(n\), where \(P_n(x)/Q_n(x)\) is the \(n\)-th Lüroth convergent of \(x\) and \(Q_n(x)\) its Lüroth denominator, has Hausdorff dimension \(0\).

Since \(0 < 1/(1 + \tau)\), the Tan–Zhou conjecture fails without monotonicity.

public theorem_wanted exists_not_antitone_dimH_lurothWellApproximableSet_eq_zero (τ : ℝ)
    (hτ : 0 ≤ τ) :
    ∃ ψ : ℕ → ℝ, (∀ q, 0 < ψ q ∧ ψ q ≤ 1) ∧ (¬ ∃ N, AntitoneOn ψ (Set.Ici N)) ∧
      lowerOrderAtInfinity ψ = ENNReal.ofReal τ ∧ dimH (lurothWellApproximableSet ψ) = 0

Sources

• Ying Wai Lee, Lüroth Expansions in Diophantine Approximation: Metric Properties and Conjectures, INTEGERS 26 (2026), Article A45, Theorem 9.

Uses 2

Statement usesLower order at infinity · Lüroth well approximable numbers

TheoremDimension of Lüroth well approximable sets under a divergence condition#●ready to prove

Let \(\psi\) be a function from the natural numbers to \((0, 1]\). Let \(L(\psi)\) be the set of \(x \in (0, 1]\) such that \(|x - P_n(x)/Q_n(x)| < \psi(Q_n(x))/Q_n(x)\) for infinitely many \(n\), where \(P_n(x)/Q_n(x)\) is the \(n\)-th Lüroth convergent of \(x\) and \(Q_n(x)\) its Lüroth denominator. Let \(\tau_\psi = \liminf_{q \to \infty} (-\log \psi(q) / \log q)\), taken in \([0, \infty]\), be the lower order at infinity of \(1/\psi\), and suppose \(\tau_\psi > 1\). Put \(t = 1/(1 + \tau_\psi)\), with \(t = 0\) if \(\tau_\psi = \infty\), and \(\theta_t(q) = \min\{1, 2^{-t} q^{1-t} \psi(q)^t\}\). Suppose that \(\theta_t\) is non-increasing on \(\{q : q \ge 1\}\) and that the partial sums \(\sum_{q=1}^{N} -(\psi(q)/q)^t ((1 - t) \log q + t \log(\psi(q)/2))\) tend to \(+\infty\) as \(N \to \infty\). Then the Hausdorff dimension of \(L(\psi)\) is \(1/(1 + \tau_\psi)\), read as \(0\) when \(\tau_\psi = \infty\).

The paper's monotonicity of \(\theta_t\) on \(\mathbb{N}\) is taken on \(q \ge 1\) (at \(q = 0\) the formula gives \(0\)). The terms of the series need not be nonnegative, so its divergence to \(\infty\) is read as the partial sums tending to \(+\infty\).

public theorem_wanted dimH_lurothWellApproximableSet_of_tendsto_sum (ψ : ℕ → ℝ)
    (hψ0 : ∀ q, 0 < ψ q) (hψ1 : ∀ q, ψ q ≤ 1) (hτ : 1 < lowerOrderAtInfinity ψ) (t : ℝ)
    (ht : t = ((1 + lowerOrderAtInfinity ψ)⁻¹).toReal)
    (hθ : AntitoneOn (fun q : ℕ => min 1 ((2 : ℝ) ^ (-t) * (q : ℝ) ^ (1 - t) * ψ q ^ t))
      (Set.Ici 1))
    (hdiv : Tendsto (fun N : ℕ => ∑ q ∈ Finset.Icc 1 N,
        -((ψ q / q) ^ t * ((1 - t) * Real.log q + t * Real.log (ψ q / 2)))) atTop atTop) :
    dimH (lurothWellApproximableSet ψ) = (1 + lowerOrderAtInfinity ψ)⁻¹

Sources

• Ying Wai Lee, Lüroth Expansions in Diophantine Approximation: Metric Properties and Conjectures, INTEGERS 26 (2026), Article A45, Theorem 10.

Uses 2

Statement usesLower order at infinity · Lüroth well approximable numbers

27 fully proved23 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.