Polynomial moments

The integrals ∫ t in 0..1, t ^ 3 * Q ^ k appearing in Sendov.R are, for natural k, integrals of polynomials, hence exactly computable. This file computes them once and for all.

Expanding Q = 1 + bt + dt² by the binomial theorem twice gives

(1 + bt + dt²) ^ k = ∑ i < k+1, ∑ l < i+1, C(k,i) C(i,l) bˡ d^(i-l) t^(2i-l)

(Sendov.quad_pow), and integrating t ^ 3 times this term by term gives

∫ t in 0..1, t ^ 3 * Q ^ k = ∑ i < k+1, ∑ l < i+1, C(k,i) C(i,l) bˡ d^(i-l) / (2i-l+4)

(Sendov.integral_moment), with b = -2c and d = A. This is formula (M) of the informal plan. Every degree of the finite range reduces to this finite sum: even degrees use it directly with k = (n-4)/2, and odd degrees use it for k and k+1 after Sendov.integral_rpow_le has removed the square root.

Note that no hypothesis on c, A or α is needed here — the identity is a polynomial one. Feasibility is required only for the odd-degree reduction, never for the moments.

theorem Sendov.intervalIntegrable_const_mul_pow (a : ℝ) (m : ℕ) : IntervalIntegrable (fun (t : ℝ) => a * t ^ m) MeasureTheory.volume 0 1

Every monomial is interval integrable on [0,1].

theorem Sendov.quad_pow (b d t : ℝ) (k : ℕ) : (1 + b * t + d * t ^ 2) ^ k = ∑ i ∈ Finset.range (k + 1), ∑ l ∈ Finset.range (i + 1), ↑(k.choose i) * ↑(i.choose l) * b ^ l * d ^ (i - l) * t ^ (2 * i - l)

The binomial expansion of a power of a quadratic.

theorem Sendov.t3_mul_Q_pow (n : ℕ) (α t : ℝ) (k : ℕ) : t ^ 3 * Q n α t ^ k = ∑ i ∈ Finset.range (k + 1), ∑ l ∈ Finset.range (i + 1), ↑(k.choose i) * ↑(i.choose l) * (-2 * c n α) ^ l * A n α ^ (i - l) * t ^ (2 * i - l + 3)

The expansion of the integrand of Sendov.R as an explicit polynomial.

noncomputable def Sendov.mom (n : ℕ) (α : ℝ) (k : ℕ) : ℝ

The k-th moment ∫ t in 0..1, t ^ 3 * Q ^ k, as an explicit finite double sum. This is (M) of the informal plan.

Equations

• Sendov.mom n α k = ∑ i ∈ Finset.range (k + 1), ∑ l ∈ Finset.range (i + 1), ↑(k.choose i) * ↑(i.choose l) * (-2 * Sendov.c n α) ^ l * Sendov.A n α ^ (i - l) / ↑(2 * i - l + 4)

theorem Sendov.integral_moment (n : ℕ) (α : ℝ) (k : ℕ) : ∫ (t : ℝ) in 0..1, t ^ 3 * Q n α t ^ k = mom n α k

The moment formula. The integrals appearing in Sendov.R are exactly the finite double sum Sendov.mom, for every natural k, with no hypotheses at all.

theorem Sendov.integral_poly7 (a₀ a₁ a₂ a₃ a₄ : ℝ) : ∫ (t : ℝ) in 0..1, a₀ * t ^ 3 + a₁ * t ^ 4 + a₂ * t ^ 5 + a₃ * t ^ 6 + a₄ * t ^ 7 = a₀ / 4 + a₁ / 5 + a₂ / 6 + a₃ / 7 + a₄ / 8

The moments of a polynomial supported in degrees three to seven, kept as a convenience for the low degrees.