Erdős Problem 978

Reference:

• erdosproblems.com/978
• [Ho67] Hooley, C., On the power free values of polynomials. Mathematika (1967), 21--26.
• [Br11] Browning, T. D., Power-free values of polynomials. Arch. Math. (Basel) (2011), 139--150.
• [Er53] Erdős, P., Arithmetical properties of polynomials. J. London Math. Soc. (1953), 416--425.

theorem Erdos978.erdos_978.variants.sub_one {f : Polynomial ℤ} (hi : Irreducible f) (hd : 2 < f.natDegree) (hp : ∀ (x : ℕ), f.natDegree ≠ 2 ^ x) (hlc : 0 < f.leadingCoeff) : {n : ℕ | Powerfree (f.natDegree - 1) (Polynomial.eval (↑n) f)}.Infinite

Let f ∈ ℤ[X] be an irreducible polynomial with positive leading coefficient. Suppose that the degree k of f is larger than 2 and is not equal to a power of 2. Then the set of n such that f n is (k - 1)-th power free is infinite, and this is proved in [Er53].

theorem Erdos978.erdos_978.parts.i {f : Polynomial ℤ} (hi : Irreducible f) (hd : 2 < f.natDegree) (hp2 : ∀ (x : ℕ), f.natDegree ≠ 2 ^ x) (hlc : 0 < f.leadingCoeff) (hp : ∀ (p : ℕ), Nat.Prime p → ∃ (n : ℕ), ¬↑p ^ (f.natDegree - 1) ∣ Polynomial.eval (↑n) f) : {n : ℕ | Powerfree (f.natDegree - 1) (Polynomial.eval (↑n) f)}.HasPosDensity

Let f ∈ ℤ[X] be an irreducible polynomial with positive leading coefficient. Suppose that the degree k of f is larger than 2, is not equal to a power of 2, and f n has no fixed (k - 1)-th power divisors other than 1. Then the set of n such that f n is (k - 1)-th power free has positive density, and this is proved in [Ho67].

theorem Erdos978.erdos_978.variants.sub_two {f : Polynomial ℤ} (hi : Irreducible f) (hd : 9 ≤ f.natDegree) (hp : ∀ (p : ℕ), Nat.Prime p → ∃ (n : ℕ), ¬↑p ^ (f.natDegree - 1) ∣ Polynomial.eval (↑n) f) : {n : ℕ | Powerfree (f.natDegree - 2) (Polynomial.eval (↑n) f)}.Infinite

If the degree k of f is larger than or equal to 9, then the set of n such that f n is (k - 2)-th power free has infinitely many elements. This result is proved in [Br11].

theorem Erdos978.erdos_978.parts.ii : True ↔ ∀ {f : Polynomial ℤ}, Irreducible f → f.natDegree > 3 → (¬∃ (l : ℕ), f.natDegree = 2 ^ l) → 0 < f.leadingCoeff → (¬∃ (p : ℕ), Nat.Prime p ∧ ∀ (n : ℕ), ↑p ^ (f.natDegree - 1) ∣ Polynomial.eval (↑n) f) → {n : ℕ | Powerfree (f.natDegree - 2) (Polynomial.eval (↑n) f)}.Infinite

If $k > 3$ (and $k \neq 2^l$), then are there infinitely many $n$ for which $f(n)$ is $(k-2)$-power-free?

theorem Erdos978.erdos_978.parts.iii : True ↔ {n : ℕ | Squarefree (n ^ 4 + 2)}.Infinite

Does n ^ 4 + 2 represent infinitely many squarefree numbers?