Normal numbers

DefinitionBase-\(b\) digits of a real number#✓fully proved

For natural numbers \(b\) and \(n\) and a real number \(x\), the \(n\)-th digit of \(x\) in base \(b\), counting from \(n = 0\) just after the radix point, is \(\lfloor b^{n+1} \{x\} \rfloor \bmod b\), where \(\{x\} = x - \lfloor x \rfloor\) is the fractional part of \(x\).

For \(b \ge 2\) these are the digits of the base-\(b\) expansion of \(\{x\}\) that does not end in an infinite run of the digit \(b - 1\). The formula is intended only for bases \(b \ge 2\).

noncomputable def digitSeq (b : ℕ) (x : ℝ) (n : ℕ) : ℕ :=
  ⌊(b : ℝ) ^ (n + 1) * Int.fract x⌋₊ % b

Used by 3

Used byNormal numbers · Simply normal numbers · Normal numbers are simply normal

DefinitionSimply normal numbers#✓fully proved

For a natural number \(b\) and a real number \(x\), write \(a_k\) for the \(k\)-th base-\(b\) digit of \(x\) after the radix point, counting from \(k = 0\). Then \(x\) is simply normal in base \(b\) if for every natural number \(d < b\) the proportion \(\#\{k < n : a_k = d\} / n\) tends to \(1/b\) as \(n \to \infty\).

This predicate is intended for bases \(b \ge 2\).

noncomputable def IsSimplyNormalInBase (b : ℕ) (x : ℝ) : Prop :=
  ∀ d : ℕ, d < b →
    Tendsto
      (fun n : ℕ =>
        (((Finset.range n).filter (fun k => digitSeq b x k = d)).card : ℝ) / n)
      atTop
      (nhds (1 / (b : ℝ)))

Uses 1 · Used by 1

Statement usesBase-\(b\) digits of a real number

Used byNormal numbers are simply normal

DefinitionNormal numbers#✓fully proved

For a natural number \(b\) and a real number \(x\), write \(a_i\) for the \(i\)-th base-\(b\) digit of \(x\) after the radix point, counting from \(i = 0\). Then \(x\) is normal in base \(b\) if for every natural number \(k\) and all natural numbers \(w_0, \dots, w_{k-1} < b\) the proportion \(\#\{i < n : a_{i+j} = w_j \text{ for all } j < k\} / n\) tends to \(1/b^k\) as \(n \to \infty\).

This predicate is intended for bases \(b \ge 2\).

noncomputable def IsNormalInBase (b : ℕ) (x : ℝ) : Prop :=
  ∀ (k : ℕ) (w : Fin k → ℕ), (∀ j, w j < b) →
    Tendsto
      (fun n : ℕ =>
        (((Finset.range n).filter
          (fun i => ∀ j : Fin k, digitSeq b x (i + j) = w j)).card : ℝ) / n)
      atTop
      (nhds (1 / (b : ℝ) ^ k))

Uses 1 · Used by 3

Statement usesBase-\(b\) digits of a real number

Used byAbsolutely normal numbers · Normal numbers are simply normal · Campbell's concatenation of \(h_2\) is not normal in base \(10\)

TheoremNormal numbers are simply normal#✓fully proved

If a real number \(x\) is normal in base \(b\), then \(x\) is simply normal in base \(b\).

theorem IsNormalInBase.isSimplyNormalInBase {b : ℕ} {x : ℝ} (h : IsNormalInBase b x) :
    IsSimplyNormalInBase b x

Uses 3

Statement usesNormal numbers · Simply normal numbers

Proof usesBase-\(b\) digits of a real number

DefinitionAbsolutely normal numbers#✓fully proved

A real number is absolutely normal if it is normal in every base at least two.

noncomputable def IsAbsolutelyNormal (x : ℝ) : Prop :=
  ∀ b : ℕ, 2 ≤ b → IsNormalInBase b x

Uses 1

Statement usesNormal numbers

DefinitionCampbell's sequence \(h_1\)#✓fully proved

For a natural number \(n\), \(h_1(n) = 0\) if \(n < 10\) and \(h_1(n) = 10^{\lfloor \log_{10} n \rfloor}\) if \(n \ge 10\); thus for \(n \ge 10\), \(h_1(n)\) is the largest power of \(10\) that is at most \(n\).

def campbellH1 (n : ℕ) : ℕ :=
  if n < 10 then 0 else 10 ^ Nat.log 10 n

Sources

• John M. Campbell, A Counterexample to a Purported Construction of Normal Numbers, Journal of Integer Sequences 29 (2026), Article 26.3.4, Section 2 (definition of h₁).

Used by 3

Used bySmall values of \(h_1\) · Sums of \(h_1\) and the jumps of \(h_2\) at powers of ten · Campbell's sequence \(h_2\)

TheoremSmall values of \(h_1\)#✓fully proved

Campbell's auxiliary sequence \(h_1\) satisfies \(h_1(9) = 0\), \(h_1(10) = 10\), \(h_1(99) = 10\) and \(h_1(100) = 100\).

theorem campbellH1_small :
    campbellH1 9 = 0 ∧ campbellH1 10 = 10 ∧ campbellH1 99 = 10 ∧ campbellH1 100 = 100

Sources

• John M. Campbell, A Counterexample to a Purported Construction of Normal Numbers, Journal of Integer Sequences 29 (2026), Article 26.3.4, Section 2.

Uses 1

Statement usesCampbell's sequence \(h_1\)

DefinitionCampbell's sequence \(h_2\)#✓fully proved

For a natural number \(n\), let \(k = \lfloor \log_{10} n \rfloor\) (with \(k = 0\) for \(n = 0\)), let \(h_1\) be Campbell's sequence and let \(S_k = \sum_{i=1}^{10^k} h_1(i)\). Then \(h_2(n) = 10^k \lfloor S_k / 10^k \rfloor + \sum_{i=10^k+1}^{n} h_1(i)\), where the last sum is empty when \(n \le 10^k\).

This is OEIS A380904.

def campbellH2 (n : ℕ) : ℕ :=
  10 ^ Nat.log 10 n * ((∑ i ∈ Finset.Icc 1 (10 ^ Nat.log 10 n), campbellH1 i) / 10 ^ Nat.log 10 n) +
    ∑ i ∈ Finset.Icc (10 ^ Nat.log 10 n + 1) n, campbellH1 i

Sources

• John M. Campbell, A Counterexample to a Purported Construction of Normal Numbers, Journal of Integer Sequences 29 (2026), Article 26.3.4, Section 2, Equation (6) (definition of h₂).

Uses 1 · Used by 8

Statement usesCampbell's sequence \(h_1\)

Used byDecimal digit block of \(h_2(n)\) · Campbell's interpolation · Campbell's interpolation on \((100/11, 10)\) · Sums of \(h_1\) and the jumps of \(h_2\) at powers of ten · Small values of Campbell's sequence \(h_2\) · Campbell's auxiliary function \(h_3^{(m)}\) · First piece of Campbell's auxiliary function \(h_3^{(m)}\) · The floor of Campbell's interpolation at positive integers is Campbell's sequence \(h_2\)

TheoremSmall values of Campbell's sequence \(h_2\)#✓fully proved

The sequence \(h_2\) satisfies \(h_2(9) = 0\), \(h_2(10) = 10\), \(h_2(21) = 120\), \(h_2(99) = 900\) and \(h_2(100) = 1000\).

theorem campbellH2_small :
    campbellH2 9 = 0 ∧ campbellH2 10 = 10 ∧ campbellH2 21 = 120 ∧ campbellH2 99 = 900 ∧
      campbellH2 100 = 1000

Sources

• John M. Campbell, A Counterexample to a Purported Construction of Normal Numbers, Journal of Integer Sequences 29 (2026), Article 26.3.4, Example 1 and Section 2.1.

Uses 1

Statement usesCampbell's sequence \(h_2\)

DefinitionCampbell's auxiliary function \(h_3^{(m)}\)#✓fully proved

For a natural number \(m\), let \(H(m) = h_2(10^m) - h_2(10^m - 1)\), where \(h_2\) is Campbell's sequence (in the paper's notation \(H(m) = y_1(m + 1) - y_2(m)\) with \(y_1(n) = h_2(10^{n-1})\) and \(y_2(n) = h_2(10^n - 1)\)). Define \(h_3^{(m)} : \mathbb{R} \to \mathbb{R}\) by \(h_3^{(m)}(t) = a(m)\,t + b(m)\) for \(t \le 10^m - 1/10\) and \(h_3^{(m)}(t) = c(m)\,t + d(m)\) for \(t > 10^m - 1/10\), where \(a(m) = (20H(m) - 11 \cdot 10^m)/9 + 9 \cdot 10^{m-1}\), \(b(m) = (10^m - 1)(-20H(m) + 11 \cdot 10^m)/9 + 10^m - 9 \cdot 10^{2m-1}\), \(c(m) = -20H(m) + 9 \cdot 10^{m-1} + 11 \cdot 10^m\) and \(d(m) = 20 \cdot 10^m H(m) - 11 \cdot 10^{2m} - 9 \cdot 10^{2m-1} + 10^m\), with the exponents \(m - 1\) and \(2m - 1\) read as \(0\) when \(m = 0\).

The paper uses \(h_3^{(m)}\) only on \([10^m - 1, 10^m]\) for \(m \ge 2\).

noncomputable def campbellH3 (m : ℕ) (t : ℝ) : ℝ :=
  let H : ℝ := (campbellH2 (10 ^ m) : ℝ) - campbellH2 (10 ^ m - 1)
  if t ≤ 10 ^ m - 1 / 10 then
    ((20 * H - 11 * 10 ^ m) / 9 + 9 * 10 ^ (m - 1)) * t +
      ((10 ^ m - 1) * (-20 * H + 11 * 10 ^ m) / 9 + 10 ^ m - 9 * 10 ^ (2 * m - 1))
  else
    (-20 * H + 9 * 10 ^ (m - 1) + 11 * 10 ^ m) * t +
      (20 * 10 ^ m * H - 11 * 10 ^ (2 * m) - 9 * 10 ^ (2 * m - 1) + 10 ^ m)

Sources

• John M. Campbell, A Counterexample to a Purported Construction of Normal Numbers, Journal of Integer Sequences 29 (2026), Article 26.3.4, Section 2.2, Equations (16)-(20).

Uses 1 · Used by 3

Statement usesCampbell's sequence \(h_2\)

Used byCampbell's interpolation · Campbell's interpolation on \((100/11, 10)\) · First piece of Campbell's auxiliary function \(h_3^{(m)}\)

TheoremFirst piece of Campbell's auxiliary function \(h_3^{(m)}\)#✓fully proved

For every natural number \(m\) and every real number \(t \le 10^m - 1/10\), \(h_3^{(m)}(t) = a(m)\,t + b(m)\), where \(H(m) = h_2(10^m) - h_2(10^m - 1)\) with \(h_2\) Campbell's sequence, \(a(m) = (20H(m) - 11 \cdot 10^m)/9 + 9 \cdot 10^{m-1}\) and \(b(m) = (10^m - 1)(-20H(m) + 11 \cdot 10^m)/9 + 10^m - 9 \cdot 10^{2m-1}\), with the exponents \(m - 1\) and \(2m - 1\) read as \(0\) when \(m = 0\).

theorem campbellH3_of_le {m : ℕ} {t : ℝ} (ht : t ≤ 10 ^ m - 1 / 10) :
    campbellH3 m t =
      ((20 * ((campbellH2 (10 ^ m) : ℝ) - campbellH2 (10 ^ m - 1)) - 11 * 10 ^ m) / 9 +
          9 * 10 ^ (m - 1)) * t +
        ((10 ^ m - 1) * (-20 * ((campbellH2 (10 ^ m) : ℝ) - campbellH2 (10 ^ m - 1)) +
            11 * 10 ^ m) / 9 + 10 ^ m - 9 * 10 ^ (2 * m - 1))

Sources

• John M. Campbell, A Counterexample to a Purported Construction of Normal Numbers, Journal of Integer Sequences 29 (2026), Article 26.3.4, Section 2.2.

Uses 2

Statement usesCampbell's sequence \(h_2\) · Campbell's auxiliary function \(h_3^{(m)}\)

DefinitionCampbell's interpolation#✓fully proved

Let \(h_2\) be Campbell's sequence and \(h_3^{(m)}\) the auxiliary piecewise-linear functions of the construction, and for \(n \ge 1\) put \(y_1(n) = h_2(10^{n-1})\) and \(y_2(n) = h_2(10^n - 1)\). Campbell's interpolation is the function \(f : \mathbb{R} \to \mathbb{R}\) with \(f(x) = \frac{89}{110} e^{(100/89)(11x - 100)} + \frac{1}{10}\) for \(x \le 100/11\) and \(f(x) = 10x - 90\) for \(100/11 < x \le 10\). For \(x > 10\) put \(m = \lfloor \log_{10} \lfloor x \rfloor \rfloor + 1\), so that \(m \ge 2\) and \(10^{m-1} \le x < 10^m\); then

\[ f(x) = \frac{x (y_2(m) - y_1(m)) - (y_1(m) + 10^{m-1} y_2(m) - 10^m y_1(m))}{9 \cdot 10^{m-1} - 1} \]

if \(x \le 10^m - 1\), and \(f(x) = h_2(10^m - 1) + \int_{10^m - 1}^{x} h_3^{(m)}(t) \, dt\) if \(x > 10^m - 1\).

The paper defines \(f\) on \([0, \infty)\) only; here the first formula is used for every \(x \le 100/11\). At a power of ten \(x = 10^{m-1} > 10\) the formula for index \(m\) is used; the piece to its left takes the same value there.

noncomputable def campbellF (x : ℝ) : ℝ :=
  if x ≤ 100 / 11 then 89 / 110 * Real.exp (100 / 89 * (11 * x - 100)) + 1 / 10
  else if x ≤ 10 then 10 * x - 90
  else
    let m := Nat.log 10 ⌊x⌋₊ + 1
    let y₁ : ℝ := campbellH2 (10 ^ (m - 1))
    let y₂ : ℝ := campbellH2 (10 ^ m - 1)
    if x ≤ 10 ^ m - 1 then
      (x * (y₂ - y₁) - (y₁ + 10 ^ (m - 1) * y₂ - 10 ^ m * y₁)) / (9 * 10 ^ (m - 1) - 1)
    else
      y₂ + ∫ t in ((10 : ℝ) ^ m - 1)..x, campbellH3 m t

Sources

• John M. Campbell, A Counterexample to a Purported Construction of Normal Numbers, Journal of Integer Sequences 29 (2026), Article 26.3.4, Section 2.2, Equations (15) and (21).

Uses 2 · Used by 6

Statement usesCampbell's sequence \(h_2\) · Campbell's auxiliary function \(h_3^{(m)}\)

Used byDifferentiability of Campbell's interpolation · Monotonicity of Campbell's interpolation · Campbell's interpolation on \((100/11, 10)\) · The floor of Campbell's interpolation at positive integers is Campbell's sequence \(h_2\) · Growth exponent of Campbell's interpolation · Growth exponent of the derivative of Campbell's interpolation

TheoremCampbell's interpolation on \((100/11, 10)\)#✓fully proved

For every real \(x\) with \(100/11 < x \le 10\), Campbell's interpolation satisfies \(f(x) = 10x - 90\).

theorem campbellF_of_mem {x : ℝ} (h₁ : 100 / 11 < x) (h₂ : x ≤ 10) : campbellF x = 10 * x - 90

Sources

• John M. Campbell, A Counterexample to a Purported Construction of Normal Numbers, Journal of Integer Sequences 29 (2026), Article 26.3.4, Section 2.2.

Uses 3

Statement usesCampbell's interpolation

Proof usesCampbell's sequence \(h_2\) · Campbell's auxiliary function \(h_3^{(m)}\)

DefinitionDecimal digit block of \(h_2(n)\)#✓fully proved

For a natural number \(n\), the block of \(n\) is the list of base-\(10\) digits of \(h_2(n)\), where \(h_2\) is Campbell's sequence, written most significant digit first; when \(h_2(n) = 0\) the block is the single digit \(0\).

def campbellBlock (n : ℕ) : List ℕ :=
  if campbellH2 n = 0 then [0] else (Nat.digits 10 (campbellH2 n)).reverse

Sources

• John M. Campbell, A Counterexample to a Purported Construction of Normal Numbers, Journal of Integer Sequences 29 (2026), Article 26.3.4, Section 1.1 (the expansion 0.b₁b₂… with b_n the base-g expansion of ⌊f(n)⌋).

Uses 1 · Used by 1

Statement usesCampbell's sequence \(h_2\)

Used byDigits of the concatenation \(0.h_2(1)h_2(2)\ldots\)

DefinitionDigits of the concatenation \(0.h_2(1)h_2(2)\ldots\)#✓fully proved

Let \(h_2\) be Campbell's sequence. For \(j \ge 0\), \(d_j\) is the digit in position \(j\) (counting from \(0\)) after the decimal point of \(0.h_2(1)h_2(2)\ldots\), the string obtained by writing the blocks of \(h_2(1), h_2(2), \ldots\) one after another, where the block of \(h_2(n)\) is its list of base-\(10\) digits, most significant first, with \(0\) written as the single digit \(0\).

Every block is nonempty, so \(d_j\) already lies in the first \(j + 1\) blocks.

def campbellConcatDigit (j : ℕ) : ℕ :=
  ((List.range (j + 1)).flatMap fun i => campbellBlock (i + 1)).getD j 0

Sources

• John M. Campbell, A Counterexample to a Purported Construction of Normal Numbers, Journal of Integer Sequences 29 (2026), Article 26.3.4, Theorem 8 (the concatenation 0.h₂(1)h₂(2)…).

Uses 1 · Used by 2

Statement usesDecimal digit block of \(h_2(n)\)

Used byThe first eleven digits of the concatenation \(0.h_2(1)h_2(2)\ldots\) · Campbell's constant

TheoremThe first eleven digits of the concatenation \(0.h_2(1)h_2(2)\ldots\)#✓fully proved

Let \(h_2\) be Campbell's sequence and let \(d_0, d_1, d_2, \ldots\) be the digits after the decimal point of \(0.h_2(1)h_2(2)\ldots\), the concatenation of the base-\(10\) digit blocks of \(h_2(1), h_2(2), \ldots\) (with \(0\) written as the single digit \(0\)). Then \((d_0, d_1, \ldots, d_{10}) = (0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0)\): nine zero blocks from \(h_2(1) = \cdots = h_2(9) = 0\), then the block of \(h_2(10) = 10\).

theorem campbellConcatDigit_small :
    (List.range 11).map campbellConcatDigit = [0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0]

Sources

• John M. Campbell, A Counterexample to a Purported Construction of Normal Numbers, Journal of Integer Sequences 29 (2026), Article 26.3.4, Example 1.

Uses 1

Statement usesDigits of the concatenation \(0.h_2(1)h_2(2)\ldots\)

DefinitionCampbell's constant#✓fully proved

Let \(h_2\) be Campbell's sequence. Campbell's constant is the real number \(\sum_{j \ge 0} d_j \, 10^{-(j+1)} = 0.d_0 d_1 d_2 \ldots\), where \(d_0, d_1, d_2, \ldots\) are the digits after the decimal point of the concatenation \(0.h_2(1)h_2(2)\ldots\) of the base-\(10\) digit blocks of \(h_2(1), h_2(2), \ldots\) (with \(0\) written as the single digit \(0\)).

noncomputable def campbellConstant : ℝ :=
  ∑' j : ℕ, (campbellConcatDigit j : ℝ) / 10 ^ (j + 1)

Sources

• John M. Campbell, A Counterexample to a Purported Construction of Normal Numbers, Journal of Integer Sequences 29 (2026), Article 26.3.4, Theorem 8.

Uses 1 · Used by 1

Statement usesDigits of the concatenation \(0.h_2(1)h_2(2)\ldots\)

Used byCampbell's concatenation of \(h_2\) is not normal in base \(10\)

TheoremSums of \(h_1\) and the jumps of \(h_2\) at powers of ten#●ready to prove

Let \(h_1\) be Campbell's auxiliary sequence and \(h_2\) Campbell's sequence. For every integer \(\ell \ge 1\), \(\sum_{i=1}^{10^{\ell+1}-1} h_1(i) = \sum_{j=0}^{\ell-1} 900 \cdot 100^j\), the number written \(9090\cdots900\) (\(\ell\) blocks \(90\), then \(0\)). Moreover, writing \(y_1(n) = h_2(10^{n-1})\) and \(y_2(n) = h_2(10^n - 1)\), for every integer \(\ell \ge 2\) we have \((y_2(\ell) - y_1(\ell)) / (9 \cdot 10^{\ell-1} - 1) = 10^{\ell-1}\) and \(y_1(\ell + 1) - y_2(\ell) = 10^{2\lfloor \ell/2 \rfloor}\).

public theorem_wanted campbellH1_sum_and_y_relations :
    (∀ ℓ : ℕ, 1 ≤ ℓ →
      ∑ i ∈ Finset.Icc 1 (10 ^ (ℓ + 1) - 1), campbellH1 i = ∑ j ∈ Finset.range ℓ, 900 * 100 ^ j) ∧
    ∀ ℓ : ℕ, 2 ≤ ℓ →
      ((campbellH2 (10 ^ ℓ - 1) : ℚ) - campbellH2 (10 ^ (ℓ - 1))) / (9 * 10 ^ (ℓ - 1) - 1) =
          10 ^ (ℓ - 1) ∧
        (campbellH2 (10 ^ ℓ) : ℤ) - campbellH2 (10 ^ ℓ - 1) = 10 ^ (2 * (ℓ / 2))

Sources

• John M. Campbell, A Counterexample to a Purported Construction of Normal Numbers, Journal of Integer Sequences 29 (2026), Article 26.3.4, Lemma 2 (jis-2026-26.3.4-lem-2).

Uses 2

Statement usesCampbell's sequence \(h_1\) · Campbell's sequence \(h_2\)

TheoremThe floor of Campbell's interpolation at positive integers is Campbell's sequence \(h_2\)#●ready to prove

Let \(f\) be Campbell's interpolation and \(h_2\) Campbell's sequence. For every integer \(n \ge 1\), \(\lfloor f(n) \rfloor = h_2(n)\), and for every integer \(n \ge 10\), \(f(n) = h_2(n)\).

public theorem_wanted floor_campbellF_eq_campbellH2 :
    (∀ n : ℕ, 1 ≤ n → ⌊campbellF n⌋₊ = campbellH2 n) ∧
    ∀ n : ℕ, 10 ≤ n → campbellF n = campbellH2 n

Sources

• John M. Campbell, A Counterexample to a Purported Construction of Normal Numbers, Journal of Integer Sequences 29 (2026), Article 26.3.4, Lemma 3 (jis-2026-26.3.4-lem-3).

Uses 2

Statement usesCampbell's interpolation · Campbell's sequence \(h_2\)

TheoremDifferentiability of Campbell's interpolation#●ready to prove

Campbell's interpolation \(f\) is differentiable at every real \(x > 0\).

public theorem_wanted campbellF_differentiableOn : DifferentiableOn ℝ campbellF (Set.Ioi 0)

Sources

• John M. Campbell, A Counterexample to a Purported Construction of Normal Numbers, Journal of Integer Sequences 29 (2026), Article 26.3.4, Lemma 4 (jis-2026-26.3.4-lem-4).

Uses 1

Statement usesCampbell's interpolation

TheoremMonotonicity of Campbell's interpolation#●ready to prove

Campbell's interpolation \(f\) is monotone (non-decreasing) on \([0, \infty)\): for all real numbers \(x\) and \(y\) with \(0 \le x \le y\), \(f(x) \le f(y)\).

public theorem_wanted campbellF_monotoneOn : MonotoneOn campbellF (Set.Ici 0)

Sources

• John M. Campbell, A Counterexample to a Purported Construction of Normal Numbers, Journal of Integer Sequences 29 (2026), Article 26.3.4, Lemma 5 (jis-2026-26.3.4-lem-5).

Uses 1

Statement usesCampbell's interpolation

TheoremGrowth exponent of Campbell's interpolation#●ready to prove

For Campbell's interpolation \(f\), \(\log f(x) / \log x \to 2\) as \(x \to \infty\) over the reals; that is, \(\eta(f) = 2\), where \(\eta(h) = \lim_{x \to \infty} \log h(x) / \log x\).

public theorem_wanted tendsto_log_campbellF_div_log :
    Filter.Tendsto (fun x => Real.log (campbellF x) / Real.log x) Filter.atTop (nhds 2)

Sources

• John M. Campbell, A Counterexample to a Purported Construction of Normal Numbers, Journal of Integer Sequences 29 (2026), Article 26.3.4, Lemma 6 (jis-2026-26.3.4-lem-6).

Uses 1

Statement usesCampbell's interpolation

TheoremGrowth exponent of the derivative of Campbell's interpolation#●ready to prove

For Campbell's interpolation \(f\), \(\log f'(x) / \log x \to 1\) as \(x \to \infty\) over the reals; that is, \(\eta(f') = 1\), where \(\eta(h) = \lim_{x \to \infty} \log h(x) / \log x\). Here \(f'(x)\) is taken to be \(0\) at any point where \(f\) is not differentiable, and \(\log 0 = 0\).

public theorem_wanted tendsto_log_deriv_campbellF_div_log :
    Filter.Tendsto (fun x => Real.log (deriv campbellF x) / Real.log x) Filter.atTop (nhds 1)

Sources

• John M. Campbell, A Counterexample to a Purported Construction of Normal Numbers, Journal of Integer Sequences 29 (2026), Article 26.3.4, Lemma 7 (jis-2026-26.3.4-lem-7).

Uses 1

Statement usesCampbell's interpolation

TheoremCampbell's concatenation of \(h_2\) is not normal in base \(10\)#●ready to prove

Let \(h_2\) be Campbell's sequence and let \(c_0, c_1, c_2, \ldots\) be the base-\(10\) digits of \(h_2(1), h_2(2), \ldots\), each number written most significant digit first and the numbers written one after another (with \(h_2(n) = 0\) written as the single digit \(0\)). The real number \(\sum_{j \ge 0} c_j 10^{-(j+1)} = 0.c_0c_1c_2\ldots\) is not normal in base \(10\).

public theorem_wanted not_isNormalInBase_campbellConstant :
    ¬ NormalNumber.IsNormalInBase 10 campbellConstant

Sources

• John M. Campbell, A Counterexample to a Purported Construction of Normal Numbers, Journal of Integer Sequences 29 (2026), Article 26.3.4, Theorem 8 (jis-2026-26.3.4-thm-8).

Uses 2

Statement usesNormal numbers · Campbell's constant

17 fully proved7 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.