Random multiplicative functions

DefinitionRademacher measure on the integer units#✓fully proved

The Rademacher measure is the uniform probability measure on the two integer units \(\{-1, 1\}\).

noncomputable def rademacherMeasure : Measure ℤˣ :=
  Measure.uniformOfFinset Finset.univ

Used by 4

Used byExistence of a Rademacher family · Rademacher family · Measurability of the prime signs · Each Rademacher sign has probability one half

TheoremEach Rademacher sign has probability one half#✓fully proved

For each integer unit \(x \in \{-1, 1\}\), the Rademacher measure of the singleton \(\{x\}\) is \(1/2\).

theorem rademacherMeasure_singleton (x : ℤˣ) :
    rademacherMeasure {x} = (2 : ENNReal)⁻¹

Uses 1

Statement usesRademacher measure on the integer units

DefinitionRademacher family#✓fully proved

Let \(\mu\) be a measure on a measurable space \(\Omega\). A family \((X_p)\), indexed by the primes \(p\), of maps \(X_p \colon \Omega \to \{-1, 1\}\) into the units of \(\mathbb{Z}\) is a Rademacher family for \(\mu\) when every \(X_p\) is measurable, every \(X_p\) has law the Rademacher measure (the uniform measure on \(\{-1, 1\}\)) under \(\mu\), and the family is mutually independent under \(\mu\).

def IsRademacherFamily {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω)
    (X : Nat.Primes → Ω → ℤˣ) : Prop :=
  (∀ p, Measurable (X p)) ∧ (∀ p, HasLaw (X p) rademacherMeasure μ) ∧ iIndepFun X μ

Uses 1 · Used by 4

Statement usesRademacher measure on the integer units

Used byRademacher LIL constant conjecture · Existence of a Rademacher family · Measurability of the prime signs · Measurability of the Rademacher random multiplicative function

TheoremExistence of a Rademacher family#✓fully proved

There exist a measurable space \(\Omega\), a probability measure \(\mu\) on \(\Omega\) and a family \((X_p)\), indexed by the primes \(p\), of maps \(X_p \colon \Omega \to \{-1, 1\}\) into the units of \(\mathbb{Z}\) that is a Rademacher family for \(\mu\).

theorem exists_rademacherFamily :
    ∃ (Ω : Type) (_ : MeasurableSpace Ω) (μ : Measure Ω) (X : Nat.Primes → Ω → ℤˣ),
      IsRademacherFamily μ X ∧ IsProbabilityMeasure μ

Uses 2

Statement usesRademacher family

Proof usesRademacher measure on the integer units

DefinitionPrime sign of a natural number#✓fully proved

Let \(X = (X_p)\) be a family, indexed by the primes \(p\), of maps \(X_p \colon \Omega \to \{-1, 1\}\) into the units of \(\mathbb{Z}\). For a natural number \(n\) and \(\omega \in \Omega\), the prime sign of \(n\) at \(\omega\) is the integer \(X_n(\omega)\) if \(n\) is prime and \(1\) otherwise.

def primeSignNat {Ω : Type*} (X : Nat.Primes → Ω → ℤˣ) (n : ℕ) (ω : Ω) : ℤ :=
  if h : Nat.Prime n then (X ⟨n, h⟩ ω : ℤ) else 1

Used by 8

Used byThe Rademacher random multiplicative function is multiplicative · Measurability of the prime signs · Measurability of the Rademacher random multiplicative function · Rademacher random multiplicative function · Formula for the Rademacher random multiplicative function · The Rademacher random multiplicative function on squarefree numbers · The Rademacher random multiplicative function vanishes off squarefree numbers · Value of the Rademacher function at a prime

TheoremMeasurability of the prime signs#✓fully proved

Let \((X_p)\) be a Rademacher family for a measure \(\mu\) on a measurable space \(\Omega\). For every natural number \(n\), the map \(\omega \mapsto \varepsilon_n(\omega)\) from \(\Omega\) to \(\mathbb{Z}\) is measurable, where the prime sign \(\varepsilon_n(\omega)\) is \(X_n(\omega)\) if \(n\) is prime and \(1\) otherwise.

theorem IsRademacherFamily.measurable_primeSignNat {Ω : Type*} [MeasurableSpace Ω]
    {μ : Measure Ω} {X : Nat.Primes → Ω → ℤˣ} (hX : IsRademacherFamily μ X) (n : ℕ) :
    Measurable (primeSignNat X n)

Uses 3 · Used by 1

Statement usesRademacher family · Prime sign of a natural number

Proof usesRademacher measure on the integer units

Used byMeasurability of the Rademacher random multiplicative function

DefinitionRademacher random multiplicative function#✓fully proved

Let \((X_p)_p\) be a family of maps \(X_p : \Omega \to \{-1, 1\}\) indexed by the primes, and let \(\omega \in \Omega\). The Rademacher random multiplicative function at \(\omega\) is the arithmetic function \(f : \mathbb{N} \to \mathbb{Z}\) with \(f(0) = 0\) and

\[f(n) = \mu(n)^2 \prod_{p \mid n} X_p(\omega)\]

for \(n \ge 1\), where \(\mu\) is the Möbius function and the product runs over the distinct primes \(p\) dividing \(n\).

noncomputable def rademacherFunction {Ω : Type*} (X : Nat.Primes → Ω → ℤˣ) (ω : Ω) :
    ArithmeticFunction ℤ :=
  (moebius.pmul moebius).pmul (prodPrimeFactors fun p => primeSignNat X p ω)

Uses 1 · Used by 8

Statement usesPrime sign of a natural number

Used byThe Rademacher random multiplicative function is multiplicative · Measurability of the Rademacher random multiplicative function · Partial sums of the Rademacher multiplicative function · Formula for the Rademacher random multiplicative function · The Rademacher random multiplicative function on squarefree numbers · The Rademacher random multiplicative function vanishes off squarefree numbers · Value of the Rademacher function at a prime · The Rademacher random multiplicative function vanishes at prime squares

TheoremFormula for the Rademacher random multiplicative function#✓fully proved

Let \(X = (X_p)\) be a family, indexed by the primes \(p\), of maps \(X_p \colon \Omega \to \{-1, 1\}\), let \(\omega \in \Omega\), and let \(f\) be the Rademacher random multiplicative function of \(X\) at \(\omega\). For every natural number \(n \neq 0\), \(f(n) = \mu(n)^2 \prod_{p \mid n} \varepsilon_p(\omega)\), where \(\mu\) is the Möbius function, the product runs over the distinct primes \(p\) dividing \(n\), and \(\varepsilon_p(\omega)\) is the prime sign of \(p\) at \(\omega\).

theorem rademacherFunction_apply {Ω : Type*} {X : Nat.Primes → Ω → ℤˣ} {ω : Ω}
    {n : ℕ} (hn : n ≠ 0) :
    rademacherFunction X ω n =
      ((moebius n : ℤ) ^ 2) * ∏ p ∈ n.primeFactors, primeSignNat X p ω

Uses 2 · Used by 3

Statement usesPrime sign of a natural number · Rademacher random multiplicative function

Used byMeasurability of the Rademacher random multiplicative function · The Rademacher random multiplicative function on squarefree numbers · The Rademacher random multiplicative function vanishes off squarefree numbers

TheoremThe Rademacher random multiplicative function on squarefree numbers#✓fully proved

Let \(X = (X_p)\) be a family, indexed by the primes \(p\), of maps \(X_p \colon \Omega \to \{-1, 1\}\), let \(\omega \in \Omega\), and let \(f\) be the Rademacher random multiplicative function of \(X\) at \(\omega\). For every squarefree natural number \(n\), \(f(n) = \prod_{p \mid n} \varepsilon_p(\omega)\), the product of the prime signs \(\varepsilon_p(\omega)\) at \(\omega\) over the distinct primes \(p\) dividing \(n\).

theorem rademacherFunction_eq_prod_of_squarefree {Ω : Type*}
    {X : Nat.Primes → Ω → ℤˣ} {ω : Ω} {n : ℕ} (hn : Squarefree n) :
    rademacherFunction X ω n = ∏ p ∈ n.primeFactors, primeSignNat X p ω

Uses 3 · Used by 1

Statement usesPrime sign of a natural number · Rademacher random multiplicative function

Proof usesFormula for the Rademacher random multiplicative function

Used byValue of the Rademacher function at a prime

TheoremThe Rademacher random multiplicative function vanishes off squarefree numbers#✓fully proved

Let \(X = (X_p)\) be a family, indexed by the primes \(p\), of maps \(X_p \colon \Omega \to \{-1, 1\}\), let \(\omega \in \Omega\), and let \(f\) be the Rademacher random multiplicative function of \(X\) at \(\omega\). Then \(f(n) = 0\) for every natural number \(n\) that is not squarefree, including \(n = 0\).

theorem rademacherFunction_eq_zero_of_not_squarefree {Ω : Type*}
    {X : Nat.Primes → Ω → ℤˣ} {ω : Ω} {n : ℕ} (hn : ¬Squarefree n) :
    rademacherFunction X ω n = 0

Uses 3 · Used by 1

Statement usesRademacher random multiplicative function

Proof usesPrime sign of a natural number · Formula for the Rademacher random multiplicative function

Used byThe Rademacher random multiplicative function vanishes at prime squares

TheoremThe Rademacher random multiplicative function is multiplicative#✓fully proved

Let \(X = (X_p)\) be a family, indexed by the primes \(p\), of maps \(X_p \colon \Omega \to \{-1, 1\}\), and let \(\omega \in \Omega\). The Rademacher random multiplicative function \(f\) of \(X\) at \(\omega\) satisfies \(f(1) = 1\) and \(f(mn) = f(m) f(n)\) for all coprime natural numbers \(m\) and \(n\).

theorem isMultiplicative_rademacherFunction {Ω : Type*}
    {X : Nat.Primes → Ω → ℤˣ} {ω : Ω} :
    IsMultiplicative (rademacherFunction X ω)

Uses 2

Statement usesRademacher random multiplicative function

Proof usesPrime sign of a natural number

TheoremValue of the Rademacher function at a prime#✓fully proved

Let \((X_p)_p\) be a family of maps \(X_p : \Omega \to \{-1, 1\}\) indexed by the primes, let \(\omega \in \Omega\), and let \(f\) be the associated Rademacher random multiplicative function at \(\omega\). For every prime \(p\), the value \(f(p)\) is the sign assigned to \(p\), that is, \(f(p) = X_p(\omega)\).

@[simp]
theorem rademacherFunction_prime {Ω : Type*} {X : Nat.Primes → Ω → ℤˣ} {ω : Ω}
    {p : ℕ} (hp : Nat.Prime p) :
    rademacherFunction X ω p = primeSignNat X p ω

Uses 3

Statement usesPrime sign of a natural number · Rademacher random multiplicative function

Proof usesThe Rademacher random multiplicative function on squarefree numbers

TheoremThe Rademacher random multiplicative function vanishes at prime squares#✓fully proved

Let \(X = (X_p)\) be a family, indexed by the primes \(p\), of maps \(X_p \colon \Omega \to \{-1, 1\}\), let \(\omega \in \Omega\), and let \(f\) be the Rademacher random multiplicative function of \(X\) at \(\omega\). Then \(f(p^2) = 0\) for every prime \(p\).

@[simp]
theorem rademacherFunction_prime_sq {Ω : Type*} {X : Nat.Primes → Ω → ℤˣ} {ω : Ω}
    {p : ℕ} (hp : Nat.Prime p) :
    rademacherFunction X ω (p ^ 2) = 0

Uses 2

Statement usesRademacher random multiplicative function

Proof usesThe Rademacher random multiplicative function vanishes off squarefree numbers

TheoremMeasurability of the Rademacher random multiplicative function#✓fully proved

Let \((X_p)\) be a Rademacher family for a measure \(\mu\) on a measurable space \(\Omega\), and for \(\omega \in \Omega\) let \(f_\omega\) be the Rademacher random multiplicative function of \((X_p)\) at \(\omega\). For every natural number \(n\), the map \(\omega \mapsto f_\omega(n)\) from \(\Omega\) to \(\mathbb{Z}\) is measurable.

theorem IsRademacherFamily.measurable_rademacherFunction {Ω : Type*} [MeasurableSpace Ω]
    {μ : Measure Ω} {X : Nat.Primes → Ω → ℤˣ} (hX : IsRademacherFamily μ X) (n : ℕ) :
    Measurable (fun ω => rademacherFunction X ω n)

Uses 5

Statement usesRademacher family · Rademacher random multiplicative function

Proof usesMeasurability of the prime signs · Prime sign of a natural number · Formula for the Rademacher random multiplicative function

DefinitionPartial sums of the Rademacher multiplicative function#✓fully proved

Given signs \(X_p(\omega) \in \{-1, 1\}\) indexed by the primes \(p\) and a sample point \(\omega\), and given \(N \in \mathbb{N}\), the partial sum \(S_N(\omega)\) is the real number \(\sum_{m=1}^{N} f_\omega(m)\), where \(f_\omega\) is the Rademacher multiplicative function of the signs \(X_p(\omega)\): \(f_\omega(m) = \prod_{p \mid m} X_p(\omega)\) for squarefree \(m\) and \(f_\omega(m) = 0\) otherwise.

noncomputable def partialSum {Ω : Type*} (X : Nat.Primes → Ω → ℤˣ) (ω : Ω)
    (N : ℕ) : ℝ :=
  ∑ m ∈ Finset.Icc 1 N, ((rademacherFunction X ω m : ℤ) : ℝ)

Uses 1 · Used by 1

Statement usesRademacher random multiplicative function

Used byRademacher LIL constant conjecture

DefinitionRademacher LIL constant conjecture#✓fully proved

The statement that there is a real constant \(c > 0\) such that, for every probability space \((\Omega, \mu)\) and every family \((X_p)_p\) of independent, measurable random signs indexed by the primes, each uniform on \(\{-1, 1\}\), for \(\mu\)-almost every \(\omega\) the limit superior as \(N \to \infty\) of \(S_N(\omega) / \sqrt{N \log \log N}\) equals \(c\). Here \(S_N(\omega) = \sum_{m=1}^{N} f_\omega(m)\) is the partial sum of the Rademacher random multiplicative function \(f_\omega\), given by \(f_\omega(m) = \prod_{p \mid m} X_p(\omega)\) for squarefree \(m\) and \(f_\omega(m) = 0\) otherwise.

This is the question asked in Erdős Problem 520.

def conjecture : Prop :=
  ∃ c : ℝ, 0 < c ∧ ∀ (Ω : Type) [MeasurableSpace Ω] (μ : Measure Ω)
    [IsProbabilityMeasure μ] (X : Nat.Primes → Ω → ℤˣ),
    IsRademacherFamily μ X →
    ∀ᵐ ω ∂μ, Filter.limsup
      (fun N : ℕ => partialSum X ω N /
        Real.sqrt ((N : ℝ) * Real.log (Real.log (N : ℝ)))) Filter.atTop = c

Uses 2 · Used by 1

Statement usesPartial sums of the Rademacher multiplicative function · Rademacher family

Used byNo iterated-logarithm constant for Rademacher multiplicative functions

TheoremNo iterated-logarithm constant for Rademacher multiplicative functions#●ready to prove

The Rademacher LIL constant conjecture is false: there is no real constant \(c > 0\) such that, for every probability space \((\Omega, \mu)\) and every family \((X_p)_p\) of independent, measurable random signs indexed by the primes, each uniform on \(\{-1, 1\}\), for \(\mu\)-almost every \(\omega\) the limit superior as \(N \to \infty\) of \(S_N(\omega) / \sqrt{N \log \log N}\) equals \(c\). Here \(S_N(\omega) = \sum_{m=1}^{N} f_\omega(m)\), where \(f_\omega\) is the Rademacher random multiplicative function: \(f_\omega(m) = \prod_{p \mid m} X_p(\omega)\) for squarefree \(m\) and \(f_\omega(m) = 0\) otherwise.

Durkan and Pearce-Crump, and independently Verreault, proved that for every \(\varepsilon > 0\), almost surely \(|\sum_{n \le x} f_\omega(n)| \ll \sqrt{x} (\log \log x)^{1/4 + \varepsilon}\) as \(x \to \infty\), so the normalized limit superior is almost surely \(0\).

public theorem_wanted conjecture_refuted : ¬ conjecture

Sources

• B. Durkan, A. Pearce-Crump, A sharp almost sure upper bound for partial sums of random multiplicative functions, arXiv preprint (2026), arXiv:2607.29429, https://arxiv.org/abs/2607.29429; W. Verreault, Almost sure upper bound for sums of random multiplicative functions and critical chaos, arXiv preprint (2026), arXiv:2608.21354, https://arxiv.org/abs/2608.21354.

Uses 1

Statement usesRademacher LIL constant conjecture

16 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.