erdos_1102.lower_density_Q_exists

There exists an infinite sequence $A = {a₁ < a₂ < …} ⊂ \mathsf{SF}$ where $\mathsf{SF} := \mathbb{N} \setminus \bigcup_{p} p^{2}\mathbb{N}$, i.e. the set of squarefree numbers. The set `A` has property `Q` and natural density `6 / π^2`. Equivalently, `(j / a_j) → 6/π^2` as `j → ∞`.

theorem erdos_1102.lower_density_Q_exists :
    ∃ A : ℕ → ℕ, StrictMono A ∧
    (∀ j, Squarefree (A j)) ∧
    HasPropertyQ (range A) ∧
    Tendsto (fun j : ℕ  ↦ (j / A j : ℝ)) atTop (𝓝 (6 / Real.pi^2))

Recent Submissions

No submissions yet. Be the first to attempt this problem.