Scaled auxiliary polynomial

The symmetric polynomial ∑ᵢ T(Xᵢ) and its evaluation, providing the algebraic input to the auxiliary integer in Niven's proof.

noncomputable def MvPolynomialSumX {R : Type u_1} [CommSemiring R] (T : Polynomial R) (n : ℕ) : MvPolynomial (Fin n) R

The symmetric polynomial ∑ᵢ₌₀ⁿ⁻¹ T(Xᵢ).

Equations

• MvPolynomialSumX T n = ∑ i : Fin n, (Polynomial.aeval (MvPolynomial.X i)) T

theorem aeval_MvPolynomialSumX {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] [Algebra R S] (T : Polynomial R) (n : ℕ) (a : Fin n → S) : (MvPolynomial.aeval a) (MvPolynomialSumX T n) = ∑ i : Fin n, (Polynomial.aeval (a i)) T

Evaluating ∑ᵢ₌₀ⁿ⁻¹ T(Xᵢ) at a gives ∑ᵢ₌₀ⁿ⁻¹ T(aᵢ).

theorem MvPolynomialSumX_isSymmetric {R : Type u_1} [CommSemiring R] (T : Polynomial R) (n : ℕ) : (MvPolynomialSumX T n).IsSymmetric

The polynomial ∑ᵢ₌₀ⁿ⁻¹ T(Xᵢ) is symmetric in the variables X₀, …, Xₙ₋₁.

theorem eval_MvPolynomialSumX_at_roots_eq_int {R : Type u_1} {S : Type u_2} [CommRing R] [Field S] [Algebra R S] [IsAlgClosed S] {n : ℕ} (B : Polynomial R) (T : Polynomial ℤ) (a : Fin n → S) (hmonic : B.Monic) (hroots : B.aroots S = valuesFin a) : ∃ (Q : MvPolynomial (Fin n) ℤ), (MvPolynomial.aeval a) (MvPolynomialSumX T n) = (algebraMap R S) ((MvPolynomial.aeval fun (i : Fin n) => (-1) ^ (↑i + 1) * B.coeff (n - (↑i + 1))) Q)

If a₀, …, aₙ₋₁ are the roots of a monic polynomial B, then ∑ᵢ₌₀ⁿ⁻¹ T(aᵢ) is a polynomial expression in the coefficients of B.

noncomputable def scaledMvPolynomial {R : Type u_1} {K : Type u_2} [CommSemiring R] [Semifield K] [Algebra R K] (P : Polynomial R) (c : K) (n : ℕ) : MvPolynomial (Fin n) K

For P = ∑ₖ₌₀ⁿ⁻¹ cₖ Xᵏ, this defines ∑ₖ (cₖ / cᵏ) (x₁ᵏ + ⋯ + xₙᵏ).

Equations

• scaledMvPolynomial P c n = ∑ k ∈ Finset.range (P.natDegree + 1), MvPolynomial.C ((algebraMap R K) (P.coeff k) / c ^ k) * MvPolynomial.psum (Fin n) K k

theorem aeval_scaledMvPolynomial {R : Type u_1} {K : Type u_2} [CommSemiring R] [Semifield K] [Algebra R K] (P : Polynomial R) (c : K) (n : ℕ) (a : Fin n → K) (hc : c ≠ 0) : (MvPolynomial.aeval fun (i : Fin n) => c * a i) (scaledMvPolynomial P c n) = ∑ i : Fin n, (Polynomial.aeval (a i)) P

Evaluating the scaled power-sum polynomial of P at c a gives ∑ᵢ₌₀ⁿ⁻¹ P(aᵢ).

theorem sum_aeval_Gp_eq_one_div_factorial_sum_iterate_derivative_Fp {R : Type u_1} {K : Type u_2} [CommSemiring R] [Field K] [CharZero K] [Algebra R K] (Q : Polynomial R) (p n : ℕ) (a : Fin n → K) : ∑ j : Fin n, (Polynomial.aeval (a j)) (Gp Q p) = 1 / ↑p.factorial * ∑ i ∈ Finset.Icc p (Fp Q p).natDegree, ∑ j : Fin n, (Polynomial.aeval (a j)) ((⇑Polynomial.derivative)^[i] (Fp Q p))

∑ⱼ₌₀ⁿ⁻¹ Gₚ(aⱼ) = (1 / p!) ∑ᵢ₌ₚ^deg(Fₚ) ∑ⱼ₌₀ⁿ⁻¹ Fₚ⁽ⁱ⁾(aⱼ).

noncomputable def ScaledCoeffDerivFp (T : Polynomial ℤ) (c : ℤ) (p s i k : ℕ) : ℤ

The integer coefficients cˢ⁻ᵏ · (i! / p!) · (k-Coeff of Sₚ).

Equations

• ScaledCoeffDerivFp T c p s i k = c ^ (s - k) * (↑(i.factorial / p.factorial) * (Sp T p i).coeff k)

noncomputable def RpolyFp (T : Polynomial ℤ) (c : ℤ) (p s i n : ℕ) : MvPolynomial (Fin n) ℤ

The symmetric polynomial encoding the scaled i-th derivative of Fₚ through power sums, i.e. ∑ₖ₌₀^deg(Fₚ) cˢ⁻ᵏ · (i! / p!) · (k-Coeff of Sₚ) · (X₀ᵏ + ⋯ + Xₙ₋₁ᵏ) .

Equations

• RpolyFp T c p s i n = ∑ k ∈ Finset.range ((Fp T p).natDegree + 1), MvPolynomial.C (ScaledCoeffDerivFp T c p s i k) * MvPolynomial.psum (Fin n) ℤ k

theorem ScaledCoeffDerivFp_from_Sp {K : Type u_1} [Field K] [CharZero K] [Algebra ℤ K] (T : Polynomial ℤ) (c : ℤ) (p s i k : ℕ) (hpi : p ≤ i) : ↑c ^ (s - k) / ↑p.factorial * ↑(((⇑Polynomial.derivative)^[i] (Fp T p)).coeff k) = (algebraMap ℤ K) (ScaledCoeffDerivFp T c p s i k)

((cˢ⁻ᵏ) / p!) · (k-th coeff of Fₚ⁽ⁱ⁾) = cˢ⁻ᵏ · (i! / p!) · (k-Coeff of Sₚ).

theorem aeval_RpolyFp_derivative_Fp (T : Polynomial ℤ) (c : ℤ) (p s i n : ℕ) (a : Fin n → ℂ) (hpi : p ≤ i) (hs : ((⇑Polynomial.derivative)^[i] (Fp T p)).natDegree ≤ s) (hc : c ≠ 0) : (MvPolynomial.aeval fun (m : Fin n) => ↑c * a m) (RpolyFp T c p s i n) = ↑c ^ s / ↑p.factorial * ∑ m : Fin n, (Polynomial.aeval (a m)) ((⇑Polynomial.derivative)^[i] (Fp T p))

Evaluating ``∑ₖ (cₖ / cᵏ) (x₁ᵏ + ⋯ + xₙᵏ)at(c a₀, …, c aₙ₋₁)gives the scaled sum `(cˢ / p!) ∑ⱼ₌₀ⁿ⁻¹ Fₚ⁽ⁱ⁾(aⱼ)`.

theorem RpolyFp_isSymmetric (T : Polynomial ℤ) (c : ℤ) (p s i n : ℕ) : (RpolyFp T c p s i n).IsSymmetric

The polynomial ∑ₖ₌₀^deg(Fₚ) cˢ⁻ᵏ · (i! / p!) · (k-Coeff of Sₚ) · (X₀ᵏ + ⋯ + Xₙ₋₁ᵏ) is symmetric.

theorem RpolyFp_at_c_mul_eq_poly_of_monicRescaleOf (T : Polynomial ℤ) (T' : Polynomial ℚ) (c : ℤ) (p s i d : ℕ) (a : Fin d → ℂ) (hc : c ≠ 0) (hmonic : T'.Monic) (hd : T'.natDegree = d) (hT : Polynomial.map (Int.castRingHom ℚ) T = Polynomial.C ↑c * T') (hroots' : T'.aroots ℂ = valuesFin a) : ∃ (Q : MvPolynomial (Fin d) ℤ), (MvPolynomial.aeval fun (j : Fin d) => ↑c * a j) (RpolyFp T c p s i d) = (algebraMap ℤ ℂ) ((MvPolynomial.aeval fun (j : Fin d) => (-1) ^ (↑j + 1) * (monicRescaleOf T d c).coeff (d - (↑j + 1))) Q)

Suppose that T = c T with T ∈ ℤ[X], T' ∈ ℚ[X], and c ∈ ℤ. If a₀, …, aₙ₋₁ are the roots of T' in ℂ, then evaluating ∑ₖ₌₀^deg(Fₚ) cˢ⁻ᵏ · (i! / p!) · (k-Coeff of Sₚ) · (X₀ᵏ + ⋯ + Xₙ₋₁ᵏ) at (c a₀, …, c aₙ₋₁) gives an integer polynomial expression in the coefficients T.

noncomputable def intAevalRpoly (T : Polynomial ℤ) (T' : Polynomial ℚ) (c : ℤ) (p s d : ℕ) (a : Fin d → ℂ) (hc : c ≠ 0) (hmonic : T'.Monic) (hd : T'.natDegree = d) (hT : Polynomial.map (Int.castRingHom ℚ) T = Polynomial.C ↑c * T') (hroots' : T'.aroots ℂ = valuesFin a) : ℕ → ℤ

The integer witness for evaluating ∑ₖ₌₀^deg(Fₚ) cˢ⁻ᵏ · (i! / p!) · (k-Coeff of Sₚ) · (X₀ᵏ + ⋯ + X_{d-1}ᵏ) at (c a₀, …, c a_{d-1}).

Equations

• intAevalRpoly T T' c p s d a hc hmonic hd hT hroots' i = (MvPolynomial.aeval fun (j : Fin d) => (-1) ^ (↑j + 1) * (monicRescaleOf T d c).coeff (d - (↑j + 1))) (Classical.choose ⋯)

noncomputable def intSumAevalGp (T : Polynomial ℤ) (T' : Polynomial ℚ) (c : ℤ) (d : ℕ) (a : Fin d → ℂ) (hc : c ≠ 0) (hmonic : T'.Monic) (hd : T'.natDegree = d) (hT : Polynomial.map (Int.castRingHom ℚ) T = Polynomial.C ↑c * T') (hroots' : T'.aroots ℂ = valuesFin a) : ℕ → ℤ

The integer witness for cᵖᵈ⁻¹ ∑ₘ Gₚ(aₘ).

Equations

• intSumAevalGp T T' c d a hc hmonic hd hT hroots' p = ∑ i ∈ Finset.Icc p (Fp T p).natDegree, intAevalRpoly T T' c p (p * d - 1) d a hc hmonic hd hT hroots' i

theorem SumAevalGp_as_intSumAevalGp (T : Polynomial ℤ) (T' : Polynomial ℚ) (c : ℤ) (p d : ℕ) (a : Fin d → ℂ) (hc : c ≠ 0) (hp : 0 < p) (hmonic : T'.Monic) (hd : T'.natDegree = d) (hT : Polynomial.map (Int.castRingHom ℚ) T = Polynomial.C ↑c * T') (hroots' : T'.aroots ℂ = valuesFin a) : ↑c ^ (p * d - 1) * ∑ m : Fin d, (Polynomial.aeval (a m)) (Gp T p) = ↑(intSumAevalGp T T' c d a hc hmonic hd hT hroots' p)

Suppose that T = c T with T ∈ ℤ[X], T' ∈ ℚ[X] monic of degree d, and c ∈ ℤ. If a₀, …, aₙ₋₁ are the roots of T' in ℂ, then the sum c^(p * d - 1) ∑_m Gₚ(a_m) is an integer.