erdos_1102.exists_sequence_with_P

Conversely, for any function `f : ℕ → ℕ` that goes to infinity, there exists a strictly increasing sequence `A = {a₁ < a₂ < …}` with property P such that `(a_j / j) ≤ f(j)` for all `j`.

theorem erdos_1102.exists_sequence_with_P
    (f : ℕ → ℕ) (h_inf : Tendsto f atTop atTop)
    (h_pos : ∀ n, f n ≠ 0) :
    ∃ A : ℕ → ℕ, StrictMono A ∧
    HasPropertyP (range A) ∧
    ∀ j : ℕ, (A j : ℝ) / j ≤ f j

Recent Submissions

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