Moments by a verified recurrence

Sendov.integral_moment computes ∫ t in 0..1, t ^ 3 * Q ^ k as the multinomial double sum (M). That formula is correct but has Θ(k²) terms, and expanding it with simp becomes impossible around k = 20: at n = 53 the 676-term expansion exhausts two million heartbeats.

This file computes the same integral by a recurrence instead. Clearing denominators with D = 2 (n-1) (3+α), the quadratic D * Q has integer coefficients as a polynomial in α:

D * Q t = g₀ + g₁ t + g₂ t², g₀ = D, g₁ = -2Dc, g₂ = DA,

so the coefficients of (D * Q t) ^ k in t satisfy

Rec (k+1) j = g₀ * Rec k j + g₁ * Rec k (j-1) + g₂ * Rec k (j-2),

which is just multiplication of the previous row by a fixed quadratic. Integrating term by term against t ^ 3 then gives the moment. This replaces Θ(k²) summands by k steps on vectors of length ≤ 2k+1.

The essential point is that the coefficients are held as integers, not as real expressions: a recurrence carried out symbolically over ℝ would grow its terms by a factor of three per step and reproduce the blow-up in another form. So polynomials in α are represented here by List ℤ (dense, lowest degree first) with their own arithmetic, and Sendov.pev is the evaluation homomorphism into ℝ. Everything a degree needs is then a kernel computation on integer data.

Main statements

• Sendov.pev_padd, Sendov.pev_pmul: evaluation is a ring homomorphism;
• Sendov.rev_qrow: qrow computes the coefficients of (g₀ + g₁t + g₂t²) ^ k;
• Sendov.integral_irow: integrating a row against t ^ (i+3) gives irow;
• Sendov.integral_moment_rec: the moment, via the recurrence.

Integer polynomials in α, densely represented, lowest degree first

def Sendov.pev : List ℤ → ℝ → ℝ

Evaluation of a dense integer polynomial at a real point, by Horner's rule.

Equations

• Sendov.pev [] x✝ = 0
• Sendov.pev (a :: p) x✝ = ↑a + x✝ * Sendov.pev p x✝

def Sendov.padd : List ℤ → List ℤ → List ℤ

Addition of dense integer polynomials.

Equations

• Sendov.padd [] x✝ = x✝
• Sendov.padd (a :: p) [] = a :: p
• Sendov.padd (a :: p) (b :: q) = (a + b) :: Sendov.padd p q

def Sendov.pmul : List ℤ → List ℤ → List ℤ

Multiplication of dense integer polynomials.

Equations

• Sendov.pmul [] x✝ = []
• Sendov.pmul (a :: p) x✝ = Sendov.padd (List.map (fun (b : ℤ) => a * b) x✝) (0 :: Sendov.pmul p x✝)

@[simp]

theorem Sendov.pev_nil (x : ℝ) : pev [] x = 0

@[simp]

theorem Sendov.pev_cons (a : ℤ) (p : List ℤ) (x : ℝ) : pev (a :: p) x = ↑a + x * pev p x

theorem Sendov.pev_padd (p q : List ℤ) (x : ℝ) : pev (padd p q) x = pev p x + pev q x

theorem Sendov.pev_map_mul (a : ℤ) (q : List ℤ) (x : ℝ) : pev (List.map (fun (b : ℤ) => a * b) q) x = ↑a * pev q x

theorem Sendov.pev_pmul (p q : List ℤ) (x : ℝ) : pev (pmul p q) x = pev p x * pev q x

Rows: polynomials in t whose coefficients are polynomials in α

def Sendov.rev : List (List ℤ) → ℝ → ℝ → ℝ

Evaluation of a row at α (coefficientwise) and t (by Horner's rule).

Equations

• Sendov.rev [] x✝¹ x✝ = 0
• Sendov.rev (p :: r) x✝¹ x✝ = Sendov.pev p x✝¹ + x✝ * Sendov.rev r x✝¹ x✝

def Sendov.radd : List (List ℤ) → List (List ℤ) → List (List ℤ)

Addition of rows.

Equations

• Sendov.radd [] x✝ = x✝
• Sendov.radd (p :: r) [] = p :: r
• Sendov.radd (p :: r) (q :: s) = Sendov.padd p q :: Sendov.radd r s

def Sendov.rscale (g : List ℤ) (r : List (List ℤ)) : List (List ℤ)

Multiply every coefficient of a row by a fixed polynomial in α.

Equations

• Sendov.rscale g r = List.map (Sendov.pmul g) r

@[simp]

theorem Sendov.rev_nil (α t : ℝ) : rev [] α t = 0

@[simp]

theorem Sendov.rev_cons (p : List ℤ) (r : List (List ℤ)) (α t : ℝ) : rev (p :: r) α t = pev p α + t * rev r α t

theorem Sendov.rev_radd (r s : List (List ℤ)) (α t : ℝ) : rev (radd r s) α t = rev r α t + rev s α t

theorem Sendov.rev_rscale (g : List ℤ) (r : List (List ℤ)) (α t : ℝ) : rev (rscale g r) α t = pev g α * rev r α t

theorem Sendov.rev_shift (r : List (List ℤ)) (α t : ℝ) : rev ([] :: r) α t = t * rev r α t

The recurrence

def Sendov.qstep (g₀ g₁ g₂ : List ℤ) (r : List (List ℤ)) : List (List ℤ)

One step of the recurrence: multiply a row by g₀ + g₁ t + g₂ t².

Equations

• Sendov.qstep g₀ g₁ g₂ r = Sendov.radd (Sendov.rscale g₀ r) (Sendov.radd ([] :: Sendov.rscale g₁ r) ([] :: [] :: Sendov.rscale g₂ r))

def Sendov.qrow (g₀ g₁ g₂ : List ℤ) : ℕ → List (List ℤ)

The coefficients of (g₀ + g₁ t + g₂ t²) ^ k, as a polynomial in t whose coefficients are integer polynomials in α.

Equations

• Sendov.qrow g₀ g₁ g₂ 0 = [[1]]
• Sendov.qrow g₀ g₁ g₂ k.succ = Sendov.qstep g₀ g₁ g₂ (Sendov.qrow g₀ g₁ g₂ k)

theorem Sendov.rev_qrow (g₀ g₁ g₂ : List ℤ) (k : ℕ) (α t : ℝ) : rev (qrow g₀ g₁ g₂ k) α t = (pev g₀ α + pev g₁ α * t + pev g₂ α * t ^ 2) ^ k

Integration

noncomputable def Sendov.irow : List (List ℤ) → ℕ → ℝ → ℝ

irow r i α = ∑ⱼ (coefficient j of r, at α) / (i + j + 4), the value of ∫ t in 0..1, t ^ (i+3) * rev r α t.

Equations

• Sendov.irow [] x✝¹ x✝ = 0
• Sendov.irow (p :: r) x✝¹ x✝ = Sendov.pev p x✝ / (↑x✝¹ + 4) + Sendov.irow r (x✝¹ + 1) x✝

theorem Sendov.continuous_rev (r : List (List ℤ)) (α : ℝ) : Continuous fun (t : ℝ) => rev r α t

theorem Sendov.integral_irow (r : List (List ℤ)) (i : ℕ) (α : ℝ) : ∫ (t : ℝ) in 0..1, t ^ (i + 3) * rev r α t = irow r i α

theorem Sendov.integral_moment_rec {n k : ℕ} {α D : ℝ} {g₀ g₁ g₂ : List ℤ} (hD : D ≠ 0) (hQ : ∀ (t : ℝ), D * Q n α t = pev g₀ α + pev g₁ α * t + pev g₂ α * t ^ 2) : ∫ (t : ℝ) in 0..1, t ^ 3 * Q n α t ^ k = irow (qrow g₀ g₁ g₂ k) 0 α / D ^ k

The moment, by the recurrence. If D * Q t has the integer coefficient polynomials g₀, g₁, g₂ in α, then the moment is a kernel computation on those integers. No hypothesis beyond D ≠ 0 is needed: this is a polynomial identity.

The coefficients for a given degree

With D = 2 (n-1) (3+α) one has D * Q t = g₀ + g₁ t + g₂ t² where, as polynomials in α with integer coefficients,

g₀ = 6(n-1) + 2(n-1) α, g₁ = -12(n-1) + (12 - 2(n-1)) α + 4 α², g₂ = 6(n-1) + (2(n-1) - 12) α - 4 α².

def Sendov.gg0 (n : ℕ) : List ℤ

D itself, as an integer polynomial in α.

Equations

• Sendov.gg0 n = [6 * (↑n - 1), 2 * (↑n - 1)]

def Sendov.gg1 (n : ℕ) : List ℤ

-2 D c, as an integer polynomial in α.

Equations

• Sendov.gg1 n = [-12 * (↑n - 1), 12 - 2 * (↑n - 1), 4]

def Sendov.gg2 (n : ℕ) : List ℤ

D A, as an integer polynomial in α.

Equations

• Sendov.gg2 n = [6 * (↑n - 1), 2 * (↑n - 1) - 12, -4]

@[simp]

theorem Sendov.gg0_length (n : ℕ) : (gg0 n).length = 2

@[simp]

theorem Sendov.gg1_length (n : ℕ) : (gg1 n).length = 3

@[simp]

theorem Sendov.gg2_length (n : ℕ) : (gg2 n).length = 3

theorem Sendov.DQ_eq (n : ℕ) (hn : 2 ≤ n) (α t : ℝ) (hα : 0 ≤ α) : 2 * M n * (3 + α) * Q n α t = pev (gg0 n) α + pev (gg1 n) α * t + pev (gg2 n) α * t ^ 2

theorem Sendov.integral_moment_of (n k : ℕ) (hn : 2 ≤ n) (α : ℝ) (hα : 0 ≤ α) : ∫ (t : ℝ) in 0..1, t ^ 3 * Q n α t ^ k = irow (qrow (gg0 n) (gg1 n) (gg2 n) k) 0 α / (2 * M n * (3 + α)) ^ k

The moment for a given degree, by the recurrence. Every ingredient on the right is a kernel computation on integers, apart from the final evaluation at α.