Calculus on polynomials

The integral ∫₀¹ x · exp(-(t · x)) · T(t · x) dt and the polynomial ∑ᵢ T⁽ⁱ⁾, together with the calculus identities relating them for Niven's argument.

noncomputable def intExpNegPoly (T : Polynomial ℤ) (x : ℂ) : ℂ

The integral ∫₀¹ x * exp(-(t * x)) * T(t * x) dt.

Equations

• intExpNegPoly T x = ∫ (t : ℝ) in 0..1, (fun (t : ℝ) => x * Complex.exp (-(↑t * x)) * (Polynomial.aeval (↑t * x)) T) t

noncomputable def sumDeriv {R : Type u_1} [Semiring R] (T : Polynomial R) : Polynomial R

The polynomial ∑ᵢ₌₀ᵈ T⁽ⁱ⁾ with d = deg(T).

Equations

• sumDeriv T = ∑ i ∈ Finset.range (T.natDegree + 1), (⇑Polynomial.derivative)^[i] T

theorem iteratedDeriv_aeval_fun (T : Polynomial ℤ) (k : ℕ) : (iteratedDeriv k fun (z : ℂ) => (Polynomial.aeval z) T) = fun (z : ℂ) => (Polynomial.aeval z) ((⇑Polynomial.derivative)^[k] T)

The k-th derivative of z ↦ T(z) is z ↦ T⁽ᵏ⁾(z).

theorem int_exp_neg_mul_poly (T : Polynomial ℤ) (x : ℂ) : intExpNegPoly T x = (Polynomial.aeval 0) (sumDeriv T) - Complex.exp (-x) * (Polynomial.aeval x) (sumDeriv T)

The equality ∫₀¹ x * exp(-(t x)) * T(t x) dt = ∑ᵢ₌₀ᵈ T⁽ⁱ⁾(0) - e^(-x) * ∑ᵢ₌₀ᵈ T⁽ⁱ⁾(x).

theorem aeval_sumDeriv_eq_sum_Icc (T : Polynomial ℤ) (a : ℂ) (m : ℕ) (hm : m ≤ Polynomial.rootMultiplicity a (Polynomial.map (algebraMap ℤ ℂ) T)) : (Polynomial.aeval a) (sumDeriv T) = ∑ i ∈ Finset.Icc m T.natDegree, (Polynomial.aeval a) ((⇑Polynomial.derivative)^[i] T)

If the multiplicity of a is ≥ m, then ∑ᵢ₌₀ᵈ T⁽ⁱ⁾(a) = ∑ᵢ₌ₘᵈ T⁽ⁱ⁾(a).

theorem T_bounded (T : Polynomial ℤ) (a : ℂ) : ∃ (M : ℝ), ∀ t ∈ Set.uIoc 0 1, ‖(Polynomial.aeval (↑t * a)) T‖ ≤ M

On the segment 0 < t ≤ 1, the values ‖T(t a)‖ are bounded above by a real constant.