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, \dots, h(n) ^ n - 1$ are collectively coprime.

Equations

• Erdos770.h n = sInf {m : ℕ∞ | 2 < m ∧ (Finset.image (fun (i : ℕ) => i ^ n - 1) (Finset.Icc 2 m.toNat)).gcd id = 1}

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

n + 1 is prime iff h n = n + 1.

theorem Erdos770.erdos_770.variants.odd_h_unbounded : Set.Unbounded (fun (x1 x2 : ℕ) => x1 ≤ x2) (ENat.toNat '' (h '' Odd))

For odd n, the values of h n form an unbounded set.

theorem Erdos770.erdos_770.parts.i : True ↔ ∀ (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.parts.ii : True ↔ Filter.liminf h Filter.atTop = ⊤

Does liminf h n = ∞?

theorem Erdos770.erdos_770.parts.iii : True ↔ ∀ ε > 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.variants.three : {n : ℕ | h n = 3}.Infinite

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