Erdős Problem 951

References:

• erdosproblems.com/951
• [Er77c] Erdős, Paul, Problems and results on combinatorial number theory. III. Number theory day (Proc. Conf., Rockefeller Univ., New York, 1976) (1977), 43-72.

def Erdos951.Erdos951_prop (a : ℕ → ℝ) : Prop

A sequence a : ℕ → ℝ is said to have property Erdos951_prop if for any pair of distinct Beuring integers x, y, |x - y| ≥ 1.

Equations

• Erdos951.Erdos951_prop a = ∀ ⦃x y : ℝ⦄, x ≠ y → x ∈ BeurlingInteger a → y ∈ BeurlingInteger a → |x - y| ≥ 1

theorem Erdos951.erdos_951.isBeurlingPrimes {a : ℕ → ℝ} (ha : 1 < a 0) (hm : StrictMono a) (he : Erdos951_prop a) : IsBeurlingPrimes a

If a has property Erdos951_prop and 1 < a 0, then a is a set of Beurling prime numbers.

theorem Erdos951.erdos_951 : sorry ↔ ∀ (a : ℕ → ℝ), Erdos951_prop a → ∀ (x : ℝ), {i : ℕ | a i ≤ x}.ncard ≤ ⌊x⌋₊.primeCounting

If a has property Erdos951_prop, is it true that #{a i ≤ x} ≤ π x?

theorem Erdos951.erdos_951.variants.beurling (a : ℕ → ℝ) : IsBeurlingPrimes a → (fun (x : ℝ) => ↑(BeurlingInteger a ∩ Set.Iic x).ncard - x) =o[Filter.atTop] Real.log → a = Nat.cast ∘ Nat.nth Nat.Prime

Beurling conjectured that if the number of Beurling integer in [1, x] is x + o(log x), then a must be the sequence of primes.