The final asymptotic passage

Once the zero count and kernel energy have their required normalized limits, the two finite-height inequalities turn into the claimed eventual proportion bounds.

theorem ZetaZeros.tendsto_ratio_of_tendsto_div_scale (N S scale : ℝ → ℝ) (C : ℝ) (hN : Filter.Tendsto (fun (T : ℝ) => N T / scale T) Filter.atTop (nhds 1)) (hS : Filter.Tendsto (fun (T : ℝ) => S T / scale T) Filter.atTop (nhds C)) (hscale : ∀ᶠ (T : ℝ) in Filter.atTop, scale T ≠ 0) : Filter.Tendsto (fun (T : ℝ) => S T / N T) Filter.atTop (nhds C)

Dividing two quantities normalized by the same eventually non-zero scale preserves their quotient limit.

theorem ZetaZeros.eventually_simple_proportion (N A S : ℝ → ℝ) (C ε : ℝ) (hε : 0 < ε) (hNpos : ∀ᶠ (T : ℝ) in Filter.atTop, 0 < N T) (hS : Filter.Tendsto (fun (T : ℝ) => S T / N T) Filter.atTop (nhds C)) (hbound : ∀ᶠ (T : ℝ) in Filter.atTop, 2 * N T - S T ≤ A T) : ∀ᶠ (T : ℝ) in Filter.atTop, 2 - C - ε < A T / N T

The simple-real lower bound gives the eventual simple-zero proportion once the kernel energy per zero tends to C.

theorem ZetaZeros.eventually_distinct_proportion (N A S : ℝ → ℝ) (C ε : ℝ) (hε : 0 < ε) (hNpos : ∀ᶠ (T : ℝ) in Filter.atTop, 0 < N T) (hS : Filter.Tendsto (fun (T : ℝ) => S T / N T) Filter.atTop (nhds C)) (hbound : ∀ᶠ (T : ℝ) in Filter.atTop, 3 / 2 * N T - S T / 2 ≤ A T) : ∀ᶠ (T : ℝ) in Filter.atTop, 3 / 2 - C / 2 - ε < A T / N T

The distinct-element lower bound gives the eventual distinct-zero proportion once the kernel energy per zero tends to C.