Skip to content

Erdős problem 25

Let n1<n2<n_1 < n_2 < \dots be an arbitrary sequence of integers, each with an associated residue class ai(modni)a_i \pmod{n_i}. Let AA be the set of integers nn such that for every ii either n<nin < n_i or n≢ai(modni)n \not\equiv a_i \pmod{n_i}. Must the logarithmic density of AA exist?

Sources

Browse retained paths and inspect the exact material available for this Problem.

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

25.lean

Retained formal statement1 of 1

Let n1<n2<n_1 < n_2 < \dots be an arbitrary sequence of integers, each with an associated residue class ai(modni)a_i \pmod{n_i}. Let AA be the set of integers nn such that for every ii either n<nin < n_i or n≢ai(modni)n \not\equiv a_i \pmod{n_i}. Must the logarithmic density of AA exist?

FormalConjectures/ErdosProblems/25.leanErdos25.erdos_254 linesExact file
True  ∀ (seq_n : ℕ → ℕ) (seq_a : ℕ → ℤ),    (∀ (i : ℕ), 0 < seq_n i) →      StrictMono seq_n → ∃ d, {x | ∀ (i : ℕ), ↑x < ↑(seq_n i) ∨ ¬↑xseq_a i [ZMOD ↑(seq_n i)]}.HasLogDensity d
OpenStatement only, no proof

Search problems.science

Find a Problem, Result, source, or page