Density of integers by their k-th smallest prime factor

DefinitionThe \(k\)-th smallest prime factor#✓fully proved

For natural numbers \(k\), \(n\) and \(p\), \(p\) is the \(k\)-th smallest prime factor of \(n\) when \(n \ne 0\), \(p\) is a prime dividing \(n\), and exactly \(k - 1\) primes dividing \(n\) are smaller than \(p\).

For \(k = 0\) the count \(k - 1\) is read as \(0\) (truncated subtraction), so \(k = 0\) and \(k = 1\) agree.

def IsKthSmallestPrimeFactor (k n p : ℕ) : Prop :=
  p ∈ Nat.primeFactors n ∧
    ((Nat.primeFactors n).filter (fun q => q < p)).card = k - 1

Used by 1

Used byThe \(k\)-th prime-factor density

DefinitionThe \(k\)-th prime-factor density#✓fully proved

For natural numbers \(k\) and \(p\), let \(S_{k,p}\) be the set of natural numbers whose \(k\)-th smallest prime factor is \(p\). The \(k\)-th prime-factor density \(d_k(p)\) is the natural density of \(S_{k,p}\), that is, the limit of \(\lvert S_{k,p} \cap \{0, 1, \dots, N - 1\} \rvert / N\) as \(N \to \infty\), when this limit exists; otherwise \(d_k(p)\) is an unspecified real number.

noncomputable def kthPrimeFactorDensity (k p : ℕ) : ℝ :=
  Classical.epsilon (fun d : ℝ =>
    Set.HasDensity {n : ℕ | IsKthSmallestPrimeFactor k n p} d)

Uses 2 · Used by 1

Statement usesThe \(k\)-th smallest prime factor · Density of a set

Used byErdős Problem 690

DefinitionUnimodality on the primes#✓fully proved

A function \(f \colon \mathbb{N} \to \mathbb{R}\) is unimodal on the primes if there is a prime \(p_0\) such that \(f(p) \le f(q)\) for all primes \(p\) and \(q\) with \(p \le q \le p_0\), and \(f(q) \le f(p)\) for all primes \(p\) and \(q\) with \(p_0 \le p \le q\).

def IsUnimodalOnPrimes (f : ℕ → ℝ) : Prop :=
  ∃ p₀ : ℕ, p₀.Prime ∧
    (∀ p q : ℕ, p.Prime → q.Prime → p ≤ q → q ≤ p₀ → f p ≤ f q) ∧
    (∀ p q : ℕ, p.Prime → q.Prime → p₀ ≤ p → p ≤ q → f q ≤ f p)

Used by 1

Used byErdős Problem 690

DefinitionErdős Problem 690#✓fully proved

The proposition that for every natural number \(k \ge 1\) the \(k\)-th prime-factor density \(d_k\) is unimodal on the primes: there is a prime \(p_0\) such that \(d_k(p) \le d_k(q)\) for all primes \(p\) and \(q\) with \(p \le q \le p_0\), and \(d_k(q) \le d_k(p)\) for all primes \(p\) and \(q\) with \(p_0 \le p \le q\). Here \(d_k(p)\) is the natural density of the set of natural numbers whose \(k\)-th smallest prime factor is \(p\) (an unspecified real number if this density does not exist).

def conjecture : Prop :=
  ∀ k : ℕ, 1 ≤ k → IsUnimodalOnPrimes (kthPrimeFactorDensity k)

Uses 2 · Used by 1

Statement usesUnimodality on the primes · The \(k\)-th prime-factor density

Used byErdős Problem 690 is false

TheoremErdős Problem 690 is false#●ready to prove

There is a natural number \(k \ge 1\) such that the \(k\)-th prime-factor density \(d_k\) is not unimodal on the primes, that is, there is no prime \(p_0\) such that \(d_k(p) \le d_k(q)\) for all primes \(p\) and \(q\) with \(p \le q \le p_0\) and \(d_k(q) \le d_k(p)\) for all primes \(p\) and \(q\) with \(p_0 \le p \le q\). Here \(d_k(p)\) is the natural density of the set of natural numbers whose \(k\)-th smallest prime factor is \(p\) (an unspecified real number if this density does not exist).

Cambie (Theorem 5) proves that \(d_k\) is unimodal for \(k = 1, 2, 3\) and not unimodal for \(4 \le k \le 20\); for example \(d_4(13) = 31/5005 > d_4(17) = 206/36465 < d_4(19) = 1308/230945\).

public theorem_wanted conjecture_refuted : ¬ conjecture

Sources

• S. Cambie, Resolution of Erdős' problems about unimodularity, arXiv preprint (2025), arXiv:2501.10333, https://arxiv.org/abs/2501.10333.

Uses 1

Statement usesErdős Problem 690

4 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.