Normal numbers

A real number $x$ is normal in base $b$ if every digit $d \in \{0,1,\dots,b-1\}$ appears with asymptotic frequency $1/b$ in the base-$b$ expansion of $x$.

A number that is normal in every integer base $b \ge 2$ is called absolutely normal.

Despite extensive empirical evidence, it remains unknown whether classical constants such as $\pi$, $e$, or $\sqrt{2}$ are normal in any base.

References:

• Wikipedia, Normal number
• Wikipedia, Borel normal number

Main definitions

• digitSeq: the sequence of digits in the base-b fractional expansion of a real number.
• IsNormalInBase: a real number is normal in base b.
• IsAbsolutelyNormal: a real number is normal in every base b ≥ 2.

noncomputable def NormalNumber.digitSeq (b : ℕ) (x : ℝ) (n : ℕ) : ℕ

The n-th digit (0-indexed) after the radix point in the base-b expansion of x.

Concretely, digitSeq b x n = ⌊b^(n+1) * {x}⌋ mod b, where {x} denotes the fractional part of x.

Equations

• NormalNumber.digitSeq b x n = ⌊↑b ^ (n + 1) * Int.fract x⌋₊ % b

noncomputable def NormalNumber.IsNormalInBase (b : ℕ) (x : ℝ) : Prop

A real number x is normal in base b if every digit d < b appears with asymptotic frequency 1 / b in the base-b fractional expansion of x.

Equations

• NormalNumber.IsNormalInBase b x = ∀ d < b, Filter.Tendsto (fun (n : ℕ) => ↑{k ∈ Finset.range n | NormalNumber.digitSeq b x k = d}.card / ↑n) Filter.atTop (nhds (1 / ↑b))

noncomputable def NormalNumber.IsAbsolutelyNormal (x : ℝ) : Prop

A real number x is absolutely normal if it is normal in every integer base b ≥ 2.

Equations

• NormalNumber.IsAbsolutelyNormal x = ∀ (b : ℕ), 2 ≤ b → NormalNumber.IsNormalInBase b x