Niven polynomials

The auxiliary polynomials Fₚ = Xᵖ⁻¹ Tᵖ and basic facts about their degree, used to build the integer that drives the contradiction in Niven's proof.

noncomputable def Fp {R : Type u_1} [Semiring R] (T : Polynomial R) (p : ℕ) : Polynomial R

Fₚ = Xᵖ⁻¹ Tᵖ.

Equations

• Fp T p = Polynomial.X ^ (p - 1) * T ^ p

theorem natDegree_Fp {R : Type u_1} [Semiring R] [Nontrivial R] [NoZeroDivisors R] (T : Polynomial R) (p : ℕ) (hT : T ≠ 0) : (Fp T p).natDegree = p - 1 + p * T.natDegree

If T ≠ 0, then deg(Fₚ) = (p - 1) + p deg(T).

theorem natDegree_iterate_derivative_Fp_le {R : Type u_1} [Semiring R] [Nontrivial R] [NoZeroDivisors R] (T : Polynomial R) (p i : ℕ) (hT : T ≠ 0) : ((⇑Polynomial.derivative)^[i] (Fp T p)).natDegree ≤ p - 1 + p * T.natDegree - i

If T ≠ 0, then deg(Fₚ⁽ⁱ⁾) ≤ (p - 1) + p deg(T) - i.

theorem coeff_Fp_pred {R : Type u_1} [CommSemiring R] (T : Polynomial R) (p : ℕ) : (Fp T p).coeff (p - 1) = T.coeff 0 ^ p

The (p - 1)-th coefficient of Fₚ is T(0)ᵖ.

theorem coeff_zero_iterate_derivative_Fp_pred {R : Type u_1} [CommSemiring R] (T : Polynomial R) (p : ℕ) : ((⇑Polynomial.derivative)^[p - 1] (Fp T p)).coeff 0 = ↑(p - 1).factorial * T.coeff 0 ^ p

Fₚ⁽ᵖ⁻¹⁾(0) = (p - 1)! * T(0)ᵖ.

theorem aeval_zero_eq_cast_coeff_zero {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (P : Polynomial R) : (Polynomial.aeval 0) P = (algebraMap R A) (P.coeff 0)

P(0) is the constant coefficient of P.

theorem rootMultiplicity_npow (T : Polynomial ℤ) (a : ℂ) (p : ℕ) (hT : T ≠ 0) : Polynomial.rootMultiplicity a (Polynomial.map (algebraMap ℤ ℂ) T ^ p) = p * Polynomial.rootMultiplicity a (Polynomial.map (algebraMap ℤ ℂ) T)

If T ≠ 0, then multₐ(Tᵖ) = p * multₐ(T).

theorem rootMultiplicity_Fp (T : Polynomial ℤ) (p : ℕ) (a : ℂ) (hT : T ≠ 0) : Polynomial.rootMultiplicity a (Polynomial.map (algebraMap ℤ ℂ) (Fp T p)) = (if a = 0 then p - 1 else 0) + p * Polynomial.rootMultiplicity a (Polynomial.map (algebraMap ℤ ℂ) T)

If T ≠ 0, then multₐ(Fₚ) = p - 1 + p * multₐ(T) if a = 0 and p * multₐ(T) otherwise.

noncomputable def Sp {R : Type u_1} [Semiring R] (T : Polynomial R) (p i : ℕ) : Polynomial R

Sₚ,ᵢ is defined so that Fₚ⁽ⁱ⁾ = i! • Sₚ,ᵢ.

Equations

• Sp T p i = ∑ j ∈ ((⇑Polynomial.derivative)^[i] (Fp T p)).support, Polynomial.C ((j + i).choose i • (Fp T p).coeff (j + i)) * Polynomial.X ^ j

noncomputable def Gp {R : Type u_1} [Semiring R] (T : Polynomial R) (p : ℕ) : Polynomial R

We define Gₚ(T) = ∑ᵢ₌ₚᵈ (i! / p!) • Sₚ,ᵢ(T), where d = deg(Fₚ).

Equations

• Gp T p = ∑ i ∈ Finset.Icc p (Fp T p).natDegree, (i.factorial / p.factorial) • Sp T p i

noncomputable def Fpd (T : Polynomial ℤ) (p : ℕ) : Polynomial ℤ

F_{p,d} = ∑ᵢ₌ₚᵈ Fₚ⁽ⁱ⁾, with d = deg(Fₚ).

Equations

• Fpd T p = sumDeriv (Fp T p)

theorem iterate_derivative_Fp_eq_factorial_Sp {R : Type u_1} [Semiring R] (T : Polynomial R) (p i : ℕ) : (⇑Polynomial.derivative)^[i] (Fp T p) = i.factorial • Sp T p i

The proof that Fₚ⁽ⁱ⁾ = i! • Sₚ,ᵢ.

theorem aeval_Fpd (T : Polynomial ℤ) (p m : ℕ) (a : ℂ) (hT : T ≠ 0) (hmT : m ≤ Polynomial.rootMultiplicity a (Polynomial.map (algebraMap ℤ ℂ) T)) : (Polynomial.aeval a) (Fpd T p) = ∑ i ∈ Finset.Icc ((if a = 0 then p - 1 else 0) + p * m) (Fp T p).natDegree, (Polynomial.aeval a) ((⇑Polynomial.derivative)^[i] (Fp T p))

If multₐ(T) ≥ m, then F_{p,d}(a) is expressed in terms of Fₚ⁽ⁱ⁾(a).

noncomputable def sumStartpDerivFp {R : Type u_1} [Semiring R] (T : Polynomial R) (p : ℕ) : Polynomial R

The definition of ∑ᵢ₌ₚᵈ Fₚ⁽ⁱ⁾ with d = deg(Fₚ).

Equations

• sumStartpDerivFp T p = ∑ i ∈ Finset.Icc p (Fp T p).natDegree, (⇑Polynomial.derivative)^[i] (Fp T p)

theorem TwithRootNotZero (T : Polynomial ℤ) (a : ℂ) (hroot : a ∈ T.aroots ℂ) : T ≠ 0

If a is a root of T, then T ≠ 0.

theorem aeval_Fpd_at_nonzero (T : Polynomial ℤ) (p : ℕ) (a : ℂ) (ha : a ≠ 0) (hroot : a ∈ T.aroots ℂ) : (Polynomial.aeval a) (Fpd T p) = (Polynomial.aeval a) (sumStartpDerivFp T p)

If a ≠ 0 and a is a root of T, then F_{p,d} = ∑ᵢ₌ₚᵈ Fₚ⁽ⁱ⁾(a).

theorem aeval_Fpd_at_zero (T : Polynomial ℤ) (p : ℕ) (hp : 0 < p) (hT : T ≠ 0) : (Polynomial.aeval 0) (Fpd T p) = ↑(p - 1).factorial * (Polynomial.aeval 0) T ^ p + (Polynomial.aeval 0) (sumStartpDerivFp T p)

If 0 < p and T ≠ 0, then F_{p,d}(0) = (p - 1)! T(0)ᵖ + ∑ᵢ₌ₚᵈ Fₚ⁽ⁱ⁾(0).

theorem intExpNegPoly_sum_simp (n p : ℕ) (T : Polynomial ℤ) (a b : Fin n → ℂ) : ∑ i : Fin n, b i * Complex.exp (a i) * intExpNegPoly (Fp T p) (a i) = (Polynomial.aeval 0) (Fpd T p) * ∑ i : Fin n, b i * Complex.exp (a i) - ∑ i : Fin n, b i * (Polynomial.aeval (a i)) (Fpd T p)

∑ᵢ bᵢ exp(aᵢ) ∫₀¹ aᵢ * exp(-(t aᵢ)) * T(t aᵢ) dt is equal to F_{p,d}(0) * ∑ᵢ bᵢ exp(aᵢ) - ∑ᵢ bᵢ F_{p,d}(0)(aᵢ).

theorem factorise_sumIteratedDerivPoly {R : Type u_1} [Semiring R] (T : Polynomial R) (p : ℕ) : sumStartpDerivFp T p = Polynomial.C ↑p.factorial * Gp T p

∑ᵢ₌ₚᵈ Fₚ⁽ⁱ⁾ = p! * Gₚ.