Almost primes

DefinitionCounting almost primes#✓fully proved

For natural numbers \(k\) and \(x\), \(\pi_k(x)\) is the number of integers \(n\) with \(1 \le n \le x\) that have exactly \(k\) prime factors, counted with multiplicity. This is the counting function in Landau's theorem on almost primes.

noncomputable def almostPrimeCounting (k x : ℕ) : ℕ :=
  ((Finset.Icc 1 x).filter (fun n => Nat.IsAlmostPrime k n)).card
Sources
Used by 4
Used byErdős–Sárközy bound for almost primes · Expansion of the reciprocal logarithm of the semiprime count · Crişan–Erban expansion of the semiprime counting function · Landau's theorem on almost primes

TheoremLandau's theorem on almost primes#✓fully proved

Let \(k \ge 1\) be a natural number and, for a natural number \(x\), let \(\pi_k(x)\) be the number of integers \(n\) with \(1 \le n \le x\) that have exactly \(k\) prime factors, counted with multiplicity. Then, as the natural number \(x\) tends to infinity,

\[\pi_k(x) \sim \frac{x \, (\log \log x)^{k-1}}{(k-1)! \, \log x}.\]
public theorem landau_almostPrimeCounting_isEquivalent (k : ℕ) (hk : 1 ≤ k) :
    Asymptotics.IsEquivalent Filter.atTop
      (fun x : ℕ => (almostPrimeCounting k x : ℝ))
      (fun x : ℕ => (x : ℝ) * (Real.log (Real.log (x : ℝ))) ^ (k - 1) /
        (((k - 1).factorial : ℝ) * Real.log (x : ℝ)))
Sources
Uses 3
Statement usesCounting almost primes
Proof usesPrime number theorem implies the theta asymptotic · Prime number theorem
2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.