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).

theorem Erdos252.erdos_252_0 : Irrational (∑' (n : ℕ), ↑((ArithmeticFunction.sigma 0) n) / ↑n.factorial)

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

theorem Erdos252.erdos_252_1 : Irrational (∑' (n : ℕ), ↑((ArithmeticFunction.sigma 1) n) / ↑n.factorial)

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

theorem Erdos252.erdos_252_2 : Irrational (∑' (n : ℕ), ↑((ArithmeticFunction.sigma 2) n) / ↑n.factorial)

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

theorem Erdos252.erdos_252_3 : Irrational (∑' (n : ℕ), ↑((ArithmeticFunction.sigma 3) n) / ↑n.factorial)

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

theorem Erdos252.erdos_252_4 : Irrational (∑' (n : ℕ), ↑((ArithmeticFunction.sigma 4) n) / ↑n.factorial)

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

theorem Erdos252.erdos_252_ge_5 : sorry ↔ ∀ k ≥ 5, Irrational (∑' (n : ℕ), ↑((ArithmeticFunction.sigma k) n) / ↑n.factorial)

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

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

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

theorem Erdos252.erdos_252.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 (∑' (n : ℕ), ↑((ArithmeticFunction.sigma k) n) / ↑n.factorial)

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