noncomputable def ErdosKac.normalizedOmega (n x : ℕ) : ℝ

Normalized version of the number-of-distinct-prime-factors function: $(\nu(x) - \log\log n) / \sqrt{\log\log n}$. This is the standardization that should converge in distribution to a standard normal.

noncomputable def ErdosKac.erdosKacDensity (n : ℕ) (t : ℝ) : ℝ

Empirical density at level $t$: the fraction of integers in $[1,n]$ whose normalized omega is at least $t$. The Erdős–Kac theorem describes its limit as $n \to \infty$.

noncomputable def ErdosKac.gaussianTailProb (t : ℝ) : ℝ

The standard Gaussian upper-tail probability $\Pr(Z \ge t)$ for $Z \sim \mathcal{N}(0,1)$.

noncomputable def ErdosKac.empiricalMoment (n k : ℕ) : ℝ

The $k$-th empirical moment of normalizedOmega n · averaged uniformly over $x \in [1,n]$.

noncomputable def ErdosKac.standardNormalMoment (k : ℕ) : ℝ

The $k$-th moment of the standard normal distribution $\mathbb{E}[Z^k]$ for $Z \sim \mathcal{N}(0,1)$.

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

Mertens' theorem (second form, used here as an axiomatic input): the prime harmonic sum $\sum_{p \le n} 1/p$ differs from $\log \log n$ by a bounded constant.

theorem clt_bernoulli_sums {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {P' : MeasureTheory.Measure Ω'} [MeasureTheory.IsProbabilityMeasure P'] (Y : ℕ → Ω → ℝ) (p : ℕ → ℝ) (hY_indep : ProbabilityTheory.iIndepFun Y P) (hY_bern : ∀ (i : ℕ), ∀ᵐ (ω : Ω) ∂P, Y i ω = 0 ∨ Y i ω = 1) (hY_mean : ∀ (i : ℕ), ∫ (x : Ω), Y i x ∂P = p i) (hp_range : ∀ (i : ℕ), 0 ≤ p i ∧ p i ≤ 1) (hvar_div : Filter.Tendsto (fun (n : ℕ) => ∑ i ∈ Finset.range n, p i * (1 - p i)) Filter.atTop Filter.atTop) (Z : Ω' → ℝ) (hZ : ProbabilityTheory.HasLaw Z (ProbabilityTheory.gaussianReal 0 1) P') : MeasureTheory.TendstoInDistribution (fun (n : ℕ) (ω : Ω) => (∑ i ∈ Finset.range n, Y i ω - ∑ i ∈ Finset.range n, p i) / √(∑ i ∈ Finset.range n, p i * (1 - p i))) Filter.atTop Z (fun (x : ℕ) => P) P'

Central limit theorem for sums of independent Bernoulli variables with variances summing to infinity: the standardized partial sums converge in distribution to a standard normal.

theorem clt_bernoulli_model_moments (k : ℕ) : ∃ (b : ℕ → ℝ), Filter.Tendsto b Filter.atTop (nhds (ErdosKac.standardNormalMoment k)) ∧ Filter.Tendsto (fun (n : ℕ) => ErdosKac.empiricalMoment n k - b n) Filter.atTop (nhds 0)

Coupling step: for each $k$, the empirical $k$-th moment of normalizedOmega n · differs from a moment of an independent-Bernoulli model b n by an error vanishing as $n \to \infty$, where b n tends to the standard normal $k$-th moment.

theorem method_of_moments_tail_convergence (h : ∀ (k : ℕ), Filter.Tendsto (fun (x : ℕ) => ErdosKac.empiricalMoment x k) Filter.atTop (nhds (ErdosKac.standardNormalMoment k))) (t : ℝ) : Filter.Tendsto (fun (x : ℕ) => ErdosKac.erdosKacDensity x t) Filter.atTop (nhds (ErdosKac.gaussianTailProb t))

Method of moments: if the empirical moments converge to the standard normal moments in every order, then the empirical tail densities erdosKacDensity n t converge to $\Pr(Z \ge t)$.

theorem ErdosKac.moment_convergence_normalized_omega (k : ℕ) : Filter.Tendsto (fun (x : ℕ) => empiricalMoment x k) Filter.atTop (nhds (standardNormalMoment k))

For every $k$, the $k$-th empirical moment of normalizedOmega n · converges to the $k$-th moment of the standard normal, obtained by combining the Bernoulli-model coupling with the CLT moment limit.

theorem ErdosKac.erdos_kac (t : ℝ) : Filter.Tendsto (fun (x : ℕ) => erdosKacDensity x t) Filter.atTop (nhds (gaussianTailProb t))

Theorem 4.5.3 (Erdős–Kac 1940). For every $t \in \mathbb{R}$, $$\frac{\#\{x \le n : (\nu(x) - \log\log n)/\sqrt{\log\log n} \ge t\}}{n} \to \Pr(Z \ge t)$$ as $n \to \infty$, where $Z \sim \mathcal{N}(0,1)$.