The centroid and second origin identities

Two of the four identities of the blog post's Lemma 1 come from comparing the two factorizations of Sendov.Counterexample.Factor coefficient by coefficient, or by evaluating them at a point. Neither needs any integration.

• the centroid identity, from the coefficient of X^{n-2} in p', equivalently from p.coeff (n-1) and p'.coeff (n-2);
• the second origin identity, from p'(0).

Everything is stated division-free. The blog post writes the second origin identity as

(-1)^{n-1} (∏ zⱼ) (1 + a ∑ⱼ 1/zⱼ) = (n / ∏ qⱼ) F(1),

with a convention that singularities are removed when some zⱼ vanishes. Multiplying out, (∏ zⱼ)(∑ⱼ 1/zⱼ) is ∑ⱼ ∏_{k≠j} z_k, which is defined whether or not any zⱼ is zero, and ∏ qⱼ clears the other denominator. So the convention becomes unnecessary rather than being formalized: no junk value of 0⁻¹ is ever evaluated.

Main statements

• Sendov.sumEraseProd: ∑ⱼ ∏_{k≠j} sₖ, the division-free form of (∏ s)(∑ 1/sⱼ);
• Sendov.centroid_identity;
• Sendov.second_origin_identity.

noncomputable def Sendov.sumEraseProd (s : Multiset ℂ) : ℂ

∑ⱼ ∏_{k≠j} sₖ. This is (∏ s) · (∑ⱼ 1/sⱼ) with the denominators cleared, and unlike that expression it is well defined when some sⱼ vanishes.

Equations

• Sendov.sumEraseProd s = (Multiset.map (fun (j : ℂ) => (s.erase j).prod) s).sum

Two rewritings of the factorizations

theorem Sendov.prod_cons_eq (a : ℂ) (z : Multiset ℂ) : (Polynomial.X - Polynomial.C a) * (Multiset.map (fun (w : ℂ) => Polynomial.X - Polynomial.C w) z).prod = (Multiset.map (fun (w : ℂ) => Polynomial.X - Polynomial.C w) (a ::ₘ z)).prod

The factorization of p, with a put back into the multiset.

The centroid identity

theorem Sendov.centroid_identity {n : ℕ} {a c : ℂ} {z q : Multiset ℂ} (hn : 2 ≤ n) {p : Polynomial ℂ} (hc0 : c ≠ 0) (hzcard : z.card = n - 1) (hqcard : q.card = n - 1) (hpz : p = Polynomial.C c * ((Polynomial.X - Polynomial.C a) * (Multiset.map (fun (w : ℂ) => Polynomial.X - Polynomial.C w) z).prod)) (hpq : Polynomial.derivative p = Polynomial.C (↑n * c) * (Multiset.map (fun (w : ℂ) => Polynomial.X - Polynomial.C w) (Multiset.map (fun (v : ℂ) => a - v⁻¹) q)).prod) : (↑n - 1) * (a + z.sum) = ↑n * (Multiset.map (fun (v : ℂ) => a - v⁻¹) q).sum

The centroid identity. (n-1)(a + ∑ zⱼ) = n ∑ⱼ (a - 1/qⱼ): the centroid of the zeroes equals the centroid of the critical points.

The second origin identity

@[simp]

theorem Sendov.sumEraseProd_zero : sumEraseProd 0 = 0

theorem Sendov.sumEraseProd_cons (v : ℂ) (t : Multiset ℂ) : sumEraseProd (v ::ₘ t) = t.prod + v * sumEraseProd t

Splitting off one element, exactly as Multiset.esymm does at the top index.

theorem Sendov.prod_map_neg (s : Multiset ℂ) : (Multiset.map (fun (w : ℂ) => -w) s).prod = (-1) ^ s.card * s.prod

Negating a multiset before taking the product.

theorem Sendov.eval_prod_zero (z : Multiset ℂ) : Polynomial.eval 0 (Multiset.map (fun (w : ℂ) => Polynomial.X - Polynomial.C w) z).prod = (-1) ^ z.card * z.prod

∏ⱼ (X - zⱼ) at the origin.

theorem Sendov.eval_deriv_prod_zero (z : Multiset ℂ) : Polynomial.eval 0 (Polynomial.derivative (Multiset.map (fun (w : ℂ) => Polynomial.X - Polynomial.C w) z).prod) = -((-1) ^ z.card * sumEraseProd z)

The derivative of ∏ⱼ (X - zⱼ) at the origin. Proved by induction rather than through Polynomial.derivative_prod, which would need the evaluation of a multiset sum.

theorem Sendov.prod_inv_sub_mul {a : ℂ} (q : Multiset ℂ) : (∀ v ∈ q, v ≠ 0) → (Multiset.map (fun (v : ℂ) => v⁻¹ - a) q).prod * q.prod = (Multiset.map (fun (v : ℂ) => 1 - a * v) q).prod

∏ⱼ (1/vⱼ - a) · ∏ⱼ vⱼ = ∏ⱼ (1 - a vⱼ): clearing the denominators of the q-side.

theorem Sendov.second_origin_identity {n : ℕ} {a c : ℂ} {z q : Multiset ℂ} {p : Polynomial ℂ} (hc0 : c ≠ 0) (hzcard : z.card = n - 1) (hq0 : ∀ v ∈ q, v ≠ 0) (hpz : p = Polynomial.C c * ((Polynomial.X - Polynomial.C a) * (Multiset.map (fun (w : ℂ) => Polynomial.X - Polynomial.C w) z).prod)) (hpq : Polynomial.derivative p = Polynomial.C (↑n * c) * (Multiset.map (fun (w : ℂ) => Polynomial.X - Polynomial.C w) (Multiset.map (fun (v : ℂ) => a - v⁻¹) q)).prod) : ↑n * (Multiset.map (fun (v : ℂ) => 1 - a * v) q).prod = (-1) ^ (n - 1) * q.prod * (z.prod + a * sumEraseProd z)

The second origin identity, division-free. The blog post's form (-1)^{n-1}(∏ zⱼ)(1 + a ∑ 1/zⱼ) = (n/∏ qⱼ) F(1) after clearing both denominators.

The integral representation

theorem Sendov.continuous_deriv_seg (p : Polynomial ℂ) (a w : ℂ) : Continuous fun (t : ℝ) => Polynomial.eval (a + ↑t * (w - a)) (Polynomial.derivative p)

The integrand of the representation below is continuous.

theorem Sendov.eval_eq_integral {p : Polynomial ℂ} {a : ℂ} (hpa : Polynomial.eval a p = 0) (w : ℂ) : Polynomial.eval w p = (w - a) * ∫ (t : ℝ) in 0..1, Polynomial.eval (a + ↑t * (w - a)) (Polynomial.derivative p)

The integral representation. p(w) = (w-a) ∫₀¹ p'(a + t(w-a)) dt when a is a root of p. This is the fundamental theorem of calculus along the segment from a to w, parametrized by a real variable; it replaces the blog post's p(z) = (z-a)∫₀¹ n ∏ⱼ (t(z-a) + 1/qⱼ) dt, which is the same statement with p' already factored.

The first origin identity

theorem Sendov.first_origin_identity {n : ℕ} {a c : ℂ} {z q : Multiset ℂ} {p : Polynomial ℂ} (hc0 : c ≠ 0) (ha0 : a ≠ 0) (hzcard : z.card = n - 1) (hq0 : ∀ v ∈ q, v ≠ 0) (hpa : Polynomial.eval a p = 0) (hpz : p = Polynomial.C c * ((Polynomial.X - Polynomial.C a) * (Multiset.map (fun (w : ℂ) => Polynomial.X - Polynomial.C w) z).prod)) (hpq : Polynomial.derivative p = Polynomial.C (↑n * c) * (Multiset.map (fun (w : ℂ) => Polynomial.X - Polynomial.C w) (Multiset.map (fun (v : ℂ) => a - v⁻¹) q)).prod) : ↑n * ∫ (t : ℝ) in 0..1, (Multiset.map (fun (v : ℂ) => 1 - a * ↑t * v) q).prod = (-1) ^ (n - 1) * q.prod * z.prod

The first origin identity, division-free. The blog post's (-1)^{n-1} ∏ zⱼ = (n / ∏ qⱼ) ∫₀¹ F(t) dt with the denominator cleared, where F(t) = ∏ⱼ (1 - a t qⱼ).

The polar identity

theorem Sendov.prod_map_mul_const (b : ℂ) (s : Multiset ℂ) (f : ℂ → ℂ) : (Multiset.map (fun (v : ℂ) => b * f v) s).prod = b ^ s.card * (Multiset.map f s).prod

Pulling a constant out of a product over a multiset.

theorem Sendov.prod_inv_mul (q : Multiset ℂ) : (∀ v ∈ q, v ≠ 0) → (Multiset.map (fun (v : ℂ) => v⁻¹) q).prod * q.prod = 1

∏ⱼ (1/vⱼ) · ∏ⱼ vⱼ = 1.

theorem Sendov.prod_sub_mul_prod {n : ℕ} {a c : ℂ} {z q : Multiset ℂ} {p : Polynomial ℂ} (hc0 : c ≠ 0) (hq0 : ∀ v ∈ q, v ≠ 0) (hpz : p = Polynomial.C c * ((Polynomial.X - Polynomial.C a) * (Multiset.map (fun (w : ℂ) => Polynomial.X - Polynomial.C w) z).prod)) (hpq : Polynomial.derivative p = Polynomial.C (↑n * c) * (Multiset.map (fun (w : ℂ) => Polynomial.X - Polynomial.C w) (Multiset.map (fun (v : ℂ) => a - v⁻¹) q)).prod) : q.prod * (Multiset.map (fun (w : ℂ) => a - w) z).prod = ↑n

p'(a) two ways. (∏ⱼ qⱼ) ∏ⱼ (a - zⱼ) = n. This is what makes the polar identity usable without dividing: it is the denominator of the blog post's ∏ⱼ (1-azⱼ)/(a-zⱼ), expressed as a product.

theorem Sendov.polar_identity {n : ℕ} {a c : ℂ} {z q : Multiset ℂ} {p : Polynomial ℂ} (hc0 : c ≠ 0) (ha0 : a ≠ 0) (ha2 : a ^ 2 ≠ 1) (hzcard : z.card = n - 1) (hqcard : q.card = n - 1) (hq0 : ∀ v ∈ q, v ≠ 0) (hpa : Polynomial.eval a p = 0) (hpz : p = Polynomial.C c * ((Polynomial.X - Polynomial.C a) * (Multiset.map (fun (w : ℂ) => Polynomial.X - Polynomial.C w) z).prod)) (hpq : Polynomial.derivative p = Polynomial.C (↑n * c) * (Multiset.map (fun (w : ℂ) => Polynomial.X - Polynomial.C w) (Multiset.map (fun (v : ℂ) => a - v⁻¹) q)).prod) : q.prod * (Multiset.map (fun (w : ℂ) => 1 - a * w) z).prod = ↑n * ∫ (t : ℝ) in 0..1, (Multiset.map (fun (v : ℂ) => a + ↑t * (1 - a ^ 2) * v) q).prod

The polar identity, division-free. The blog post's ∏ⱼ (1-azⱼ)/(a-zⱼ) = ∫₀¹ ∏ⱼ (t(1-a²)qⱼ + a) dt with the denominator cleared using Sendov.prod_sub_mul_prod.