Estimating J ∑ⱼ 1/zⱼ

The origin argument needs ∑ⱼ 1/zⱼ, which the centroid identity supplies only after the inversions 1/zⱼ = conj zⱼ and 1/qⱼ = conj qⱼ are used. Those hold exactly when the points lie on the unit circle, i.e. when |J| = 1, and the defect lemma measures the failure by 1 - |J|². Conjugating the centroid identity and paying that defect gives

J ∑ⱼ 1/zⱼ = a (n-1) J - n J (x+iy) + O_≤( (n/(n-1)) (1 - |J|²) ),

which is Sendov.Jsum_estimate below. A single application of the defect lemma, to the 2(n-1) points z₁,…,z_{n-1}, conj q₁,…,conj q_{n-1}, pays for both substitutions at once.

Everything is division-free on the z side: J ∑ⱼ 1/zⱼ is written as (∏ qⱼ) · sumEraseProd z, which is well defined even when some zⱼ vanishes. That case is not excluded by hypothesis but handled: if ∏ zⱼ = 0 then at most one term of sumEraseProd z survives, so the left side is at most 1 while the right side is at least n/(n-1) > 1. On the q side no such care is needed, since the qⱼ are reciprocals and never vanish.

Main statements

• Sendov.Jsum_estimate: the estimate above;
• Sendov.sumEraseProd_norm_le_one: the degenerate case ∏ zⱼ = 0;
• Sendov.prod_mul_sum_inv: (∏ s) ∑ⱼ 1/sⱼ = sumEraseProd s when no sⱼ vanishes.

Multiset odds and ends

theorem Sendov.sum_map_sub (s : Multiset ℂ) (f g : ℂ → ℂ) : (Multiset.map (fun (v : ℂ) => f v - g v) s).sum = (Multiset.map f s).sum - (Multiset.map g s).sum

theorem Sendov.sum_map_const_sub (s : Multiset ℂ) (c : ℂ) (g : ℂ → ℂ) : (Multiset.map (fun (v : ℂ) => c - g v) s).sum = ↑s.card * c - (Multiset.map g s).sum

theorem Sendov.sum_map_re (s : Multiset ℂ) : (Multiset.map (fun (v : ℂ) => v.re) s).sum = s.sum.re

theorem Sendov.norm_sum_map_le (s : Multiset ℂ) (f : ℂ → ℂ) : ‖(Multiset.map f s).sum‖ ≤ (Multiset.map (fun (w : ℂ) => ‖f w‖) s).sum

theorem Sendov.norm_prod_le_one (s : Multiset ℂ) : (∀ w ∈ s, ‖w‖ ≤ 1) → ‖s.prod‖ ≤ 1

theorem Sendov.prod_mul_sum_inv (s : Multiset ℂ) : (∀ w ∈ s, w ≠ 0) → s.prod * (Multiset.map (fun (w : ℂ) => w⁻¹) s).sum = sumEraseProd s

(∏ s) ∑ⱼ 1/sⱼ = ∑ⱼ ∏_{k≠j} sₖ, the clearing of denominators that is valid exactly when no sⱼ vanishes.

theorem Sendov.sumEraseProd_norm_le_one (s : Multiset ℂ) : (∀ w ∈ s, ‖w‖ ≤ 1) → s.prod = 0 → ‖sumEraseProd s‖ ≤ 1

The degenerate case. If ∏ sⱼ = 0 then some sⱼ vanishes, so at most one term of ∑ⱼ ∏_{k≠j} sₖ is nonzero — and that term is a product of points of the closed unit disk.

The estimate

theorem Sendov.Jsum_estimate {n : ℕ} (hn : 2 ≤ n) {a x y : ℝ} {z q : Multiset ℂ} (hqcard : q.card = n - 1) (hz1 : ∀ w ∈ z, ‖w‖ ≤ 1) (hq1 : ∀ v ∈ q, ‖v‖ ≤ 1) (hcent : (↑n - 1) * (↑a + z.sum) = ↑n * (Multiset.map (fun (v : ℂ) => ↑a - v⁻¹) q).sum) (hxy : q.sum = (↑n - 1) * (↑x + ↑y * Complex.I)) : ‖q.prod * sumEraseProd z - (↑a * (↑n - 1) - ↑n * (↑x + ↑y * Complex.I)) * (q.prod * z.prod)‖ ≤ ↑n / (↑n - 1) * (1 - (‖q.prod‖ * ‖z.prod‖) ^ 2)

The estimate for J ∑ⱼ 1/zⱼ. Conjugating the centroid identity replaces 1/zⱼ by conj zⱼ and qⱼ by 1/conj qⱼ; the defect lemma pays for both substitutions at once.