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.Erdos951Prop (a : ℕ → ℝ) : Prop

A sequence a : ℕ → ℝ is said to have property Erdos951Prop if for any pair of distinct finitely supported sequences k l : ℕ →₀ ℕ their corresponding Beurling integers are of distance at least one apart.

Equations

• Erdos951.Erdos951Prop a = ∀ (k ℓ : ℕ →₀ ℕ), k ≠ ℓ → |beurlingInteger a k - beurlingInteger a ℓ| ≥ 1

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

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

theorem Erdos951.erdos_951 : True ↔ ∀ (a : ℕ → ℝ), 1 < a 0 → StrictMono a → Erdos951Prop a → ∀ᶠ (x : ℝ) in Filter.atTop, {i : ℕ | a i ≤ x}.ncard ≤ ⌊x⌋₊.primeCounting

If 1 < a 0 < ... has property Erdos951Prop, is it true that #{a i ≤ x} ≤ π x?

theorem Erdos951.erdos_951.variants.beurling (a : ℕ → ℝ) : IsBeurlingPrimes a → (fun (x : ℝ) => ↑(BeurlingIntegers 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.