def HardyRamanujan.omega (n : ℕ) : ℕ

$\omega(n)$, the number of distinct prime factors of $n$.

theorem HardyRamanujan.mertens_theorem : ∃ (C : ℝ), ∀ (n : ℕ), 2 ≤ n → |∑ p ∈ Finset.range (n + 1) with Nat.Prime p, 1 / ↑p - Real.log (Real.log ↑n)| ≤ C

Mertens' theorem: there exists a constant $C$ such that for all $n \ge 2$, $\Bigl| \sum_{p \le n, p\text{ prime}} 1/p - \log \log n \Bigr| \le C$.

theorem HardyRamanujan.omega_variance_bound : ∃ (C : ℝ), 0 < C ∧ ∀ᶠ (N : ℕ) in Filter.atTop, ∑ x ∈ Finset.Icc 1 N, (↑(omega x) - Real.log (Real.log ↑N)) ^ 2 ≤ C * ↑N * Real.log (Real.log ↑N)

Variance bound on $\omega$ around $\log \log N$ (a key step toward Hardy–Ramanujan): there is $C > 0$ such that, for all sufficiently large $N$, $\sum_{x = 1}^N (\omega(x) - \log \log N)^2 \le C \cdot N \log \log N$.

theorem HardyRamanujan.chebyshev_step {N : ℕ} (hN : 0 < N) {C fN μ : ℝ} (hfN : 0 < fN) (hμ : 0 < μ) (hVarN : ∑ x ∈ Finset.Icc 1 N, (↑(omega x) - μ) ^ 2 ≤ C * ↑N * μ) : ↑{x ∈ Finset.Icc 1 N | fN * √μ ≤ |↑(omega x) - μ|}.card / ↑N ≤ C / fN ^ 2

Chebyshev-type step turning the variance bound into a density bound: if $\sum_{x = 1}^N (\omega(x) - \mu)^2 \le C N \mu$, then the proportion of $x \in [1, N]$ with $|\omega(x) - \mu| \ge f_N \sqrt{\mu}$ is at most $C / f_N^2$.

theorem HardyRamanujan.hardy_ramanujan (f : ℕ → ℝ) (hf_pos : ∀ᶠ (N : ℕ) in Filter.atTop, 0 < f N) (hf_tendsto : Filter.Tendsto f Filter.atTop Filter.atTop) : Filter.Tendsto (fun (N : ℕ) => ↑{x ∈ Finset.Icc 1 N | f N * √(Real.log (Real.log ↑N)) ≤ |↑(omega x) - Real.log (Real.log ↑N)|}.card / ↑N) Filter.atTop (nhds 0)

Hardy–Ramanujan theorem (Theorem 4.5.1): for any $f(N) \to \infty$, the proportion of $x \in [1, N]$ with $|\omega(x) - \log \log N| \ge f(N) \sqrt{\log \log N}$ tends to $0$; equivalently, $\omega(x) = (1 + o(1)) \log \log N$ for almost all $x \le N$.