Erdős Problem 409

Reference: erdosproblems.com/409

theorem Erdos409.erdos_409.parts.i (n : ℕ) (hn : 0 < n) : IsLeast {i : ℕ | Nat.Prime ((fun (x : ℕ) => x.totient + 1)^[i] n)} sorry

How many iterations of $n\mapsto\phi(n) + 1$ are needed before a prime is reached?

theorem Erdos409.erdos_409.variants.termination (n : ℕ) (hn : 0 < n) : ∃ (i : ℕ), Nat.Prime ((fun (x : ℕ) => x.totient + 1)^[i] n)

If $n > 0$, then the iteration $n\mapsto\phi(n) + 1$ necessarily reaches a prime.

theorem Erdos409.erdos_409.parts.i.isTheta (c : ℕ → ℕ) (h : ∀ n > 0, IsLeast {i : ℕ | Nat.Prime ((fun (x : ℕ) => x.totient + 1)^[i] n)} (c n)) : (fun (n : ℕ) => ↑(c n)) =Θ[Filter.atTop] sorry

Let $c(n)$ be the minimum number of iterations of $n\mapsto\phi(n) + 1$ before a prime is reached. What is $\Theta(c(n))$?

theorem Erdos409.erdos_409.parts.i.isBigO (c : ℕ → ℕ) (h : ∀ n > 0, IsLeast {i : ℕ | Nat.Prime ((fun (x : ℕ) => x.totient + 1)^[i] n)} (c n)) : (fun (n : ℕ) => ↑(c n)) =O[Filter.atTop] sorry

Let $c(n)$ be the minimum number of iterations of $n\mapsto\phi(n) + 1$ before a prime is reached. Find the simplest function $g(n)$ such that $c(n) = O(g(n))$?

theorem Erdos409.erdos_409.parts.i.isLittleO (c : ℕ → ℕ) (h : ∀ n > 0, IsLeast {i : ℕ | Nat.Prime ((fun (x : ℕ) => x.totient + 1)^[i] n)} (c n)) : (fun (n : ℕ) => ↑(c n)) =o[Filter.atTop] sorry

Let $c(n)$ be the minimum number of iterations of $n\mapsto\phi(n) + 1$ before a prime is reached. Find the simplest function $g(n)$ such that $c(n) = o(g(n))$?

theorem Erdos409.erdos_409.parts.ii : True ↔ ∃ (p : ℕ) (_ : Nat.Prime p), {n : ℕ | ∃ (i : ℕ), (fun (x : ℕ) => x.totient + 1)^[i] n = p}.Infinite

Can infinitely many $n$ reach the same prime under the iteration $n\mapsto\phi(n) + 1$?

theorem Erdos409.erdos_409.parts.iii (p : ℕ) (h : Nat.Prime p) (α : ℝ) (hα : {n : ℕ | ∃ (i : ℕ), (fun (x : ℕ) => x.totient + 1)^[i] n = p}.HasDensity α) : α = sorry

What is the density of $n$ which reach any fixed prime under the iteration $n\mapsto\phi(n) + 1$?

theorem Erdos409.erdos_409.variants.sigma (n : ℕ) (hn : n > 1) : IsLeast {i : ℕ | Nat.Prime ((fun (x : ℕ) => (ArithmeticFunction.sigma 1) x - 1)^[i] n)} sorry

How many iterations of $n\mapsto\sigma(n) - 1$ are needed before a prime is reached?

theorem Erdos409.erdos_409.variants.sigma_termination (n : ℕ) (hn : n > 1) : ∃ (i : ℕ), Nat.Prime ((fun (x : ℕ) => (ArithmeticFunction.sigma 1) x - 1)^[i] n)

If $n > 1$ then the iteration $n\mapsto\sigma(n) - 1$ necessarily reaches a prime. Note: this is open — it is not clear that the σ iteration always terminates, since it is non-decreasing (unlike the φ iteration which is strictly decreasing).

theorem Erdos409.erdos_409.variants.sigma_isTheta (c : ℕ → ℕ) (h : ∀ n > 1, IsLeast {i : ℕ | Nat.Prime ((fun (x : ℕ) => (ArithmeticFunction.sigma 1) x - 1)^[i] n)} (c n)) : (fun (n : ℕ) => ↑(c n)) =Θ[Filter.atTop] sorry

Let $c(n)$ be the minimum number of iterations of $n\mapsto\sigma(n) - 1$ before a prime is reached. What is $\Theta(c(n))$?

theorem Erdos409.erdos_409.variants.sigma_isBigO (c : ℕ → ℕ) (h : ∀ n > 1, IsLeast {i : ℕ | Nat.Prime ((fun (x : ℕ) => (ArithmeticFunction.sigma 1) x - 1)^[i] n)} (c n)) : (fun (n : ℕ) => ↑(c n)) =O[Filter.atTop] sorry

Let $c(n)$ be the minimum number of iterations of $n\mapsto\sigma(n) - 1$ before a prime is reached. Find the simplest function $g(n)$ such that $c(n) = O(g(n))$?

theorem Erdos409.erdos_409.variants.sigma_isLittleO (c : ℕ → ℕ) (h : ∀ n > 1, IsLeast {i : ℕ | Nat.Prime ((fun (x : ℕ) => (ArithmeticFunction.sigma 1) x - 1)^[i] n)} (c n)) : (fun (n : ℕ) => ↑(c n)) =o[Filter.atTop] sorry

Let $c(n)$ be the minimum number of iterations of $n\mapsto\sigma(n) - 1$ before a prime is reached. Find the simplest function $g(n)$ such that $c(n) = o(g(n))$?

theorem Erdos409.erdos_409.variants.sigma_prime_termination : True ↔ ∀ n > 1, ∃ (i : ℕ), Nat.Prime ((fun (x : ℕ) => (ArithmeticFunction.sigma 1) x - 1)^[i] n)

Is it true that iterates of $n\mapsto\sigma(n) - 1$ always reach a prime?