Erdős Problem 252

References:

• erdosproblems.com/252
• [ErSt71] Erdös, P., and E. G. Straus. "Some number theoretic results." Pacific J. Math 36 (1971): 635-646.
• [ErSt74] Erdős, Paul, and Ernst Straus. "On the irrationality of certain series." Pacific journal of mathematics 55.1 (1974): 85-92.
• [ErKa54] P. Erdős, M. Kac, Amer. Math. Monthly 61 (1954), Problem 4518.
• [ScPu06] Schlage-Puchta, J. C., The irrationality of a number theoretical series. Ramanujan J. (2006), 455-460.
• [FLC07] Friedlander, J. B. and Luca, F. and Stoiciu, M., On the irrationality of a divisor function series. Integers (2007).
• [Pr22] Pratt, K., The irrationality of a divisor function series of Erdős and Kac. arXiv:2209.11124 (2022).

noncomputable def Erdos252.erdos_252_sum (k : ℕ) : ℝ

The series ∑ σ k n / n!.

Equations

• Erdos252.erdos_252_sum k = ∑' (n : ℕ), ↑((ArithmeticFunction.sigma k) n) / ↑n.factorial

theorem Erdos252.erdos_252 : sorry ↔ ∀ k ≥ 1, Irrational (erdos_252_sum k)

theorem Erdos252.erdos_252.variants.k_eq_zero : Irrational (erdos_252_sum 0)

∑ σ 0 n / n! is irrational. This is proved in [ErSt71].

theorem Erdos252.erdos_252.variants.k_eq_one : Irrational (erdos_252_sum 1)

∑ σ 1 n / n! is irrational. This is proved in [ErSt74].

theorem Erdos252.erdos_252.variants.k_eq_two : Irrational (erdos_252_sum 2)

∑ σ 2 n / n! is irrational. This is proved in [ErKa54].

theorem Erdos252.erdos_252.variants.k_eq_three : Irrational (erdos_252_sum 3)

∑ σ 3 n / n! is irrational. This is proved in [ScPu06] and [FLC07].

theorem Erdos252.erdos_252.variants.k_eq_four : Irrational (erdos_252_sum 4)

∑ σ 4 n / n! is irrational. This is proved in [Pr22].

theorem Erdos252.erdos_252.variants.k_ge_five : sorry ↔ ∀ k ≥ 5, Irrational (erdos_252_sum k)

For a fixed k ≥ 5, is ∑ σ k n / n! irrational?.

theorem Erdos252.erdos_252.variants.schinzel (hs : ∀ (fs : Finset (Polynomial ℤ)), (∀ f ∈ fs, BunyakovskyCondition f) → SchinzelCondition fs → Infinite ↑{n : ℤ | ∀ f ∈ fs, Prime (Polynomial.eval n f).natAbs}) (k : ℕ) : Irrational (erdos_252_sum k)

If Schinzel's conjecture is true, then ∑ σ k n / n! is irrational for all k. This is proved in [ScPu06].

theorem Erdos252.erdos_252.variants.prime_tuples {k : ℕ} (hk : 4 ≤ k) (hp : ∀ (a : Fin k → ℕ+) (b : Fin k → ℕ), (∀ (p : ℕ), Nat.Prime p → ∃ (n : ℕ), ¬p ∣ ∏ i : Fin k, (↑(a i) * n + b i)) → {n : ℕ | ∀ (i : Fin k), Nat.Prime (↑(a i) * n + b i)}.Infinite) : Irrational (erdos_252_sum k)

If the prime k-tuples conjecture is true, then ∑ σ k n / n! is irrational. This is proved in [FLC07].