Main theorem for primitive sets above x

This file contains the public theorem solving Erdős Problem #1196 in the quantitative form 1 + O(1 / log x). It packages the eventual choice of the cutoff Y, builds the explicit Markov layer with visiting probabilities 1 / (B_x n log n), and combines the hit-mass and normalization estimates into the final logarithmic-series bound.

Main statements

• mainTheorem

theorem PrimitiveSetsAboveX.mainTheorem : ∃ (C : ℝ) (x₀ : ℕ), ∀ ⦃x : ℕ⦄, x₀ ≤ x → ∀ {A : Set ℕ}, PrimitiveSet A → A ⊆ Set.Ici x → Summable (A.indicator fun (m : ℕ) => 1 / (↑m * Real.log ↑m)) ∧ ∑' (m : ℕ), A.indicator (fun (k : ℕ) => 1 / (↑k * Real.log ↑k)) m ≤ 1 + C / Real.log ↑x

Formal solution of Erdős Problem #1196: there exist constants C and x₀ such that for every cutoff x ≥ x₀ and every primitive set A ⊆ Ici x, the logarithmic series ∑_{a ∈ A} 1 / (a log a) is summable and bounded above by 1 + C / log x.