The formal-conjectures statement of Erdős Problem 1196

This file packages the local solution of Erdős Problem #1196 in the mathematical form used by the formal-conjectures repository. We keep the same namespace, theorem name, and primitive-set definition, but omit the repository-specific metadata attribute and answer(...) wrapper.

Main statements

• Erdos1196.IsPrimitive
• Erdos1196.erdos_1196

def Erdos1196.IsPrimitive {M : Type u_1} [CommMonoid M] (A : Set M) : Prop

Exact local copy of the primitive-set predicate used in the official formal-conjectures statement of Erdős Problem #1196.

Equations

• Erdos1196.IsPrimitive A = ∀ x ∈ A, ∀ y ∈ A, x ∣ y → Associated x y

theorem Erdos1196.erdos_1196 : ∃ (o : ℕ → ℝ), o =o[Filter.atTop] 1 ∧ ∀ x > 0, ∀ A ⊆ Set.Ici x, IsPrimitive A → ∑' (a : ↑A), 1 / (Real.log ↑↑a * ↑↑a) < 1 + o x

This is the formal-conjectures-style formulation of Erdős Problem #1196. It is deduced from PrimitiveSetsAboveX.mainTheorem by converting the local quantitative bound 1 + C / log x into an o(1) error term.