Erdős Problem 770

References:

• erdosproblems.com/770
• [Er49d] Erdös, P. "On the strong law of large numbers." Transactions of the American Mathematical Society 67.1 (1949): 51-56.
• [Ma66] Matsuyama, Noboru. "On the strong law of large numbers." Tohoku Mathematical Journal, Second Series 18.3 (1966): 259-269.

noncomputable def Erdos770.h (n : ℕ) : ℕ∞

Let h n be the minimal number such that 2 ^ n - 1, ..., (h n) ^ n - 1 are mutually coprime.

Equations

• Erdos770.h n = sInf {m : ℕ∞ | 2 < m ∧ (Set.Icc 2 m).Pairwise fun (i j : ℕ∞) => (i.toNat ^ n - 1).Coprime (j.toNat ^ n - 1)}

theorem Erdos770.Nat.Prime.h_eq_add_one {n : ℕ} : h n = ↑n + 1 ↔ Nat.Prime (n + 1)

n + 1 is prime iff h n = n + 1. #TODO: prove this theorem.

theorem Erdos770.Odd.h_unbounded {n : ℕ} (pn : Odd n) : h n = ⊤

If n is odd, then h n = ∞. #TODO: prove this theorem.

theorem Erdos770.erdos_770.density : sorry ↔ ∀ (p : ℕ), Nat.Prime p → ∃ (a : ℝ), {n : ℕ | h n = ↑p}.HasDensity a

For every prime p, does the density of integers with h n = p exist?

theorem Erdos770.erdos_770.liminf : sorry ↔ Filter.liminf h Filter.atTop = ⊤

Does liminf h n = ∞?

theorem Erdos770.erdos_770.prime : sorry ↔ ∀ ε > 0, ∀ᶠ (n : ℕ) in Filter.atTop, have p := sSup {m : ℕ | Nat.Prime m ∧ m - 1 ∣ n}; ↑p > ↑n ^ ε → h n = ↑p

Is it true that if p is the greatest prime such that p - 1 ∣ n and p > n ^ ε, then h n = p?

theorem Erdos770.erdos_770.three : {n : ℕ | h n = 3}.Infinite

It is probably true that h n = 3 for infinitely many n.