Erdős Problem 409

Reference: erdosproblems.com/409

theorem 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 erdos_409.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 erdos_409.parts.i.variants.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 erdos_409.parts.i.variants.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 erdos_409.parts.i.variants.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 erdos_409.parts.ii : (∃ (p : ℕ) (_ : Nat.Prime p), {n : ℕ | ∃ (i : ℕ), (fun (x : ℕ) => x.totient + 1)^[i] n = p}.Infinite) ↔ sorry

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

theorem 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 erdos_409.variants.sigma.parts.i (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 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.

theorem erdos_409.variants.sigma.parts.i.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 erdos_409.variants.sigma.parts.i.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 erdos_409.variants.sigma.parts.i.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 erdos_409.variants.sigma.parts.ii : (∃ (p : ℕ) (_ : Nat.Prime p), {n : ℕ | ∃ (i : ℕ), (fun (x : ℕ) => (ArithmeticFunction.sigma 1) x - 1)^[i] n = p}.Infinite) ↔ sorry

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

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

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