Cyclotomic polynomials: size of Φ_n(x) and the parity of ω(n) (Jameson, Prop. 1.20)

For n ≥ 2 and real 0 < x ≤ 1/2, Φ_n(x) lies in (1 - x, 1) when n has an even number of distinct prime factors and in (1, 1/(1 - x)) when it has an odd number. Via the palindromy X^φ(n) Φ_n(1/X) = Φ_n(X) (proved here as reverse_cyclotomic), the matching bounds around x^φ(n) hold for x ≥ 2.

Main results

• CycloParity.cyclotomic_eval_parity: n ≥ 2, 0 < x ≤ 1/2: ω(n) even ⇒ 1 - x < Φ_n(x) < 1; odd ⇒ 1 < Φ_n(x) < 1/(1-x)
• CycloParity.cyclotomic_eval_lt_one_of_even: ω(n) even ⇒ Φ_n(x) < 1 for 0 < x ≤ 1/2
• CycloParity.one_lt_cyclotomic_eval_of_odd: ω(n) odd ⇒ 1 < Φ_n(x) for 0 < x ≤ 1/2
• CycloParity.reverse_cyclotomic: Φ_n is palindromic over ℝ for n ≥ 2
• CycloParity.cyclotomic_eval_reciprocal: Φ_n(x) = x^φ(n) Φ_n(1/x) for n ≥ 2, x ≠ 0
• CycloParity.cyclotomic_eval_parity_ge_two: n ≥ 2, x ≥ 2: ω(n) even ⇒ (x-1)x^(φ-1) < Φ_n(x) < x^φ; odd ⇒ x^φ < Φ_n(x) < x^(φ+1)/(x-1)

References

• R. Whitty, Theorem of the Day, «The Bungers–Lehmer Theorem on Cyclotomic Coefficients» (Cyclotomic).
• G. J. O. Jameson, «The cyclotomic polynomials», lecture notes (Lancaster University), §1: Proposition 1.20 and Proposition 1.3 (palindromy).

theorem CycloParity.one_sub_sum_le_prod (s : Finset ℕ) (a : ℕ → ℝ) (h : ∀ i ∈ s, 0 ≤ a i ∧ a i ≤ 1) : 1 - ∑ i ∈ s, a i ≤ ∏ i ∈ s, (1 - a i)

Weierstrass: 1 - Σ aᵢ ≤ ∏ (1 - aᵢ) for aᵢ ∈ [0,1].

theorem CycloParity.sum_pow_lt (x : ℝ) (hx0 : 0 < x) (hx1 : x < 1) (S : Finset ℕ) (m : ℕ) (hS : ∀ d ∈ S, m ≤ d) : ∑ d ∈ S, x ^ d < x ^ m / (1 - x)

Σ_{d ∈ S} x^d < x^m / (1-x) if all d ∈ S are ≥ m (distinct powers).

theorem CycloParity.ratio_bounds (x : ℝ) (hx0 : 0 < x) (hx2 : x ≤ 1 / 2) (A B : Finset ℕ) (p : ℕ) (hA1 : 1 ∈ A) (hApos : ∀ a ∈ A, 1 ≤ a) (hB2 : ∀ b ∈ B, 2 ≤ b) (hpB : p ∈ B) (hA : ∀ a ∈ A, a ≠ 1 → p + 2 ≤ a) : 0 < ∏ d ∈ B, (1 - x ^ d) ∧ (1 - x) * ∏ d ∈ B, (1 - x ^ d) < ∏ d ∈ A, (1 - x ^ d) ∧ ∏ d ∈ A, (1 - x ^ d) < ∏ d ∈ B, (1 - x ^ d)

Abstract inequalities of Jameson's proof of 1.20.

theorem CycloParity.eval_cyclotomic_moebius (x : ℝ) (hx0 : 0 < x) (hx1 : x < 1) (n : ℕ) (hn : 0 < n) : Polynomial.eval x (Polynomial.cyclotomic n ℝ) = ∏ d ∈ n.divisors, (x ^ d - 1) ^ ArithmeticFunction.moebius (n / d)

Möbius inversion for the real evaluation of Φ_n.

theorem CycloParity.moebius_div_eq (n d : ℕ) (hn : Squarefree n) (hd : d ∣ n) : ArithmeticFunction.moebius (n / d) = ArithmeticFunction.moebius n * ArithmeticFunction.moebius d

theorem CycloParity.main_squarefree (x : ℝ) (hx0 : 0 < x) (hx2 : x ≤ 1 / 2) (n : ℕ) (hn : Squarefree n) (hn1 : 2 ≤ n) : (ArithmeticFunction.moebius n = 1 → 1 - x < Polynomial.eval x (Polynomial.cyclotomic n ℝ) ∧ Polynomial.eval x (Polynomial.cyclotomic n ℝ) < 1) ∧ (ArithmeticFunction.moebius n = -1 → 1 < Polynomial.eval x (Polynomial.cyclotomic n ℝ) ∧ Polynomial.eval x (Polynomial.cyclotomic n ℝ) < 1 / (1 - x))

Squarefree case of Jameson 1.20.

theorem CycloParity.omega_eq_card (n : ℕ) : ArithmeticFunction.cardDistinctFactors n = n.primeFactors.card

theorem CycloParity.moebius_eq_pow_card (n : ℕ) (hn : Squarefree n) : ArithmeticFunction.moebius n = (-1) ^ n.primeFactors.card

theorem CycloParity.cyclotomic_eval_parity (n : ℕ) (hn : 2 ≤ n) (x : ℝ) (hx0 : 0 < x) (hx2 : x ≤ 1 / 2) : (Even n.primeFactors.card → 1 - x < Polynomial.eval x (Polynomial.cyclotomic n ℝ) ∧ Polynomial.eval x (Polynomial.cyclotomic n ℝ) < 1) ∧ (Odd n.primeFactors.card → 1 < Polynomial.eval x (Polynomial.cyclotomic n ℝ) ∧ Polynomial.eval x (Polynomial.cyclotomic n ℝ) < 1 / (1 - x))

Jameson, Proposition 1.20 for 0 < x ≤ 1/2: both parities, all n ≥ 2.

theorem CycloParity.cyclotomic_eval_lt_one_of_even (n : ℕ) (hn : 2 ≤ n) (x : ℝ) (hx0 : 0 < x) (hx2 : x ≤ 1 / 2) (he : Even n.primeFactors.card) : 1 - x < Polynomial.eval x (Polynomial.cyclotomic n ℝ) ∧ Polynomial.eval x (Polynomial.cyclotomic n ℝ) < 1

theorem CycloParity.one_lt_cyclotomic_eval_of_odd (n : ℕ) (hn : 2 ≤ n) (x : ℝ) (hx0 : 0 < x) (hx2 : x ≤ 1 / 2) (ho : Odd n.primeFactors.card) : 1 < Polynomial.eval x (Polynomial.cyclotomic n ℝ) ∧ Polynomial.eval x (Polynomial.cyclotomic n ℝ) < 1 / (1 - x)

Reciprocity and the part x ≥ 2

theorem CycloParity.reverse_one_real : Polynomial.reverse 1 = 1

theorem CycloParity.reverse_prod_dom {ι : Type u_1} (s : Finset ι) (f : ι → Polynomial ℝ) : (∏ i ∈ s, f i).reverse = ∏ i ∈ s, (f i).reverse

theorem CycloParity.reverse_X_pow_sub_one (n : ℕ) : (Polynomial.X ^ n - 1).reverse = -(Polynomial.X ^ n - 1)

theorem CycloParity.reverse_cyclotomic (n : ℕ) (hn : 2 ≤ n) : (Polynomial.cyclotomic n ℝ).reverse = Polynomial.cyclotomic n ℝ

Polynomial reciprocity: reverse Φ_n = Φ_n for n ≥ 2.

theorem CycloParity.cyclotomic_eval_reciprocal (n : ℕ) (hn : 2 ≤ n) (x : ℝ) (hx : x ≠ 0) : Polynomial.eval x (Polynomial.cyclotomic n ℝ) = x ^ n.totient * Polynomial.eval (1 / x) (Polynomial.cyclotomic n ℝ)

Reciprocity evaluated: Φ_n(x) = x^φ(n) Φ_n(1/x) for n ≥ 2, x ≠ 0.

theorem CycloParity.cyclotomic_eval_parity_ge_two (n : ℕ) (hn : 2 ≤ n) (x : ℝ) (hx : 2 ≤ x) : (Even n.primeFactors.card → (x - 1) * x ^ (n.totient - 1) < Polynomial.eval x (Polynomial.cyclotomic n ℝ) ∧ Polynomial.eval x (Polynomial.cyclotomic n ℝ) < x ^ n.totient) ∧ (Odd n.primeFactors.card → x ^ n.totient < Polynomial.eval x (Polynomial.cyclotomic n ℝ) ∧ Polynomial.eval x (Polynomial.cyclotomic n ℝ) < x ^ (n.totient + 1) / (x - 1))

Jameson, Proposition 1.20 for x ≥ 2, m = φ(n), n ≥ 2.