First-entry bounds for the normalization constant

This file completes the normalization decomposition by summing the first-entry rows and proving the final estimate for the first-entry contribution to B_x.

Main statements

• normalizationFirstEntryPart_estimate

theorem PrimitiveSetsAboveX.hasSum_normalizationFirstEntryPart {x Y : ℕ} (hx : 1 ≤ x) (hsummable : ∀ {m : ℕ}, 1 ≤ m → m < x → Summable fun (q : ℕ) => if entryThreshold x Y m ≤ q then ArithmeticFunction.vonMangoldt q / (↑q * Real.log ↑(m * q) ^ 2) else 0) : HasSum (fun (n : ℕ) => normalizationFirstEntryPart x Y n) (∑ m ∈ Finset.Icc 1 (x - 1), 1 / ↑m * firstEntryTail x Y m)

If every first-entry row is summable, then the corresponding contribution to B_x is exactly the finite parent-state sum appearing in the first-entry decomposition.

theorem PrimitiveSetsAboveX.normalizationFirstEntryPart_estimate {Y : ℕ} (hY : 2 ≤ Y) : ∃ (C : ℝ), 0 < C ∧ ∃ (x₀ : ℕ), ∀ ⦃x : ℕ⦄, x₀ ≤ x → (Summable fun (n : ℕ) => normalizationFirstEntryPart x Y n) ∧ |∑' (n : ℕ), normalizationFirstEntryPart x Y n - 1| ≤ C / Real.log ↑x

For fixed Y ≥ 2, the first-entry contribution to B_x is summable and equals 1 + O(1 / log x) as x → ∞.