Erdős Problem 377

Reference: erdosproblems.com/377

@[reducible, inline]

noncomputable abbrev sumInvPrimesNotDvdCentralBinom (n : ℕ) : ℝ

The sum of the inverses of all primes smaller than $n$, which don't divide the central binom coefficient.

Equations

• sumInvPrimesNotDvdCentralBinom n = ∑ p ∈ Finset.filter (fun (p : ℕ) => Nat.Prime p) (Finset.Icc 1 n), if p ∣ (2 * n).choose n then 0 else 1 / ↑p

theorem erdos_377 : (∃ C > 0, ∀ (n : ℕ), sumInvPrimesNotDvdCentralBinom n ≤ C) ↔ sorry

Is there some absolute constant $C > 0$ such that $$ \sum_{p \leq n} 1_{p\nmid {2n \choose n}}\frac{1}{p} \leq C $$ for all $n$?

theorem erdos_377.variants.limit.i (γ₀ : ℝ) (hγ₀ : γ₀ = ∑' (k : ℕ), Real.log (↑k + 2) / 2 ^ (k + 2)) : Filter.Tendsto (fun (x : ℕ) => 1 / ↑x * ∑ n ∈ Finset.Icc 1 x, sumInvPrimesNotDvdCentralBinom n) Filter.atTop (nhds γ₀)

Erdos, Graham, Ruzsa, and Straus proved that if $$ f(n) = \sum_{p \leq n} 1_{p\nmid {2n \choose n}}\frac{1}{p} $$ and $$ \gamma_0 = \sum_{k = 2}^{\infty} \frac{\log k}{2^k} $$ then $$ \lim_{x\to\infty} \frac{1}{x}\sum_{n\leq x} f(n) = \gamma_0 $$

[EGRS75] Erdős, P. and Graham, R. L. and Ruzsa, I. Z. and Straus, E. G., On the prime factors of $(\sp{2n}\sb{n})$. Math. Comp. (1975), 83-92.

theorem erdos_377.variants.limit.ii (γ₀ : ℝ) (hγ₀ : γ₀ = ∑' (k : ℕ), Real.log (↑k + 2) / 2 ^ (k + 2)) : Filter.Tendsto (fun (x : ℕ) => 1 / ↑x * ∑ n ∈ Finset.Icc 1 x, sumInvPrimesNotDvdCentralBinom n ^ 2) Filter.atTop (nhds (γ₀ ^ 2))

Erdos, Graham, Ruzsa, and Straus proved that if $$ f(n) = \sum_{p \leq n} 1_{p\nmid {2n \choose n}}\frac{1}{p} $$ and $$ \gamma_0 = \sum_{k = 2}^{\infty} \frac{\log k}{2^k} $$ then $$ \lim_{x\to\infty} \frac{1}{x}\sum_{n\leq x} f(n)^2 = \gamma_0^2 $$

[EGRS75] Erdős, P. and Graham, R. L. and Ruzsa, I. Z. and Straus, E. G., On the prime factors of $(\sp{2n}\sb{n})$. Math. Comp. (1975), 83-92.

theorem erdos_377.variants.ae (γ₀ : ℝ) (hγ₀ : γ₀ = ∑' (k : ℕ), Real.log (↑k + 2) / 2 ^ (k + 2)) : ∃ (o : ℕ → ℝ) (_ : Filter.Tendsto o Filter.atTop (nhds 0)), ∀ᶠ (n : ℕ) in Filter.cofinite, sumInvPrimesNotDvdCentralBinom n = γ₀ + o n

Erdos, Graham, Ruzsa, and Straus proved that if $$ f(n) = \sum_{p \leq n} 1_{p\nmid {2n \choose n}}\frac{1}{p} $$ and $$ \gamma_0 = \sum_{k = 2}^{\infty} \frac{\log k}{2^k} $$ then for almost all integers $f(m) = \gamma_0 + o(1)$.

[EGRS75] Erdős, P. and Graham, R. L. and Ruzsa, I. Z. and Straus, E. G., On the prime factors of $(\sp{2n}\sb{n})$. Math. Comp. (1975), 83-92.

theorem erdos_377.variants.ub : ∃ c < 1, ∀ᶠ (n : ℕ) in Filter.atTop, sumInvPrimesNotDvdCentralBinom n ≤ c * Real.log (Real.log ↑n)

Erdos, Graham, Ruzsa, and Straus proved that if $$ f(n) = \sum_{p \leq n} 1_{p\nmid {2n \choose n}}\frac{1}{p} $$ then there is some constant $c < 1$ such that for all large $n$ $$ f(n) \leq c \log\log n. $$

[EGRS75] Erdős, P. and Graham, R. L. and Ruzsa, I. Z. and Straus, E. G., On the prime factors of $(\sp{2n}\sb{n})$. Math. Comp. (1975), 83-92.