The polar inequality, up to the branch point

The polar identity says

(∏ q) ∏ⱼ (1 - a zⱼ) = n ∫₀¹ ∏ⱼ (t(1-a²)qⱼ + a) dt, (∏ q) ∏ⱼ (a - zⱼ) = n.

The Möbius estimate |a - zⱼ| ≤ |1 - a zⱼ|, valid because zⱼ lies in the closed unit disk and a is real with |a| ≤ 1, therefore gives

n = |(∏ q) ∏ (a - zⱼ)| ≤ |(∏ q) ∏ (1 - a zⱼ)| = n |∫₀¹ ∏ⱼ (t(1-a²)qⱼ + a) dt|,

and after the integral triangle inequality

1 ≤ ∫₀¹ ∏ⱼ |a + t(1-a²)qⱼ| dt. (⋆)

(⋆) is the branch point of the whole argument. The high-degree route relaxes it by AM–GM into the raw polar inequality (1Q) of Sendov.Reduction.Setup; the low-degree route for 2 ≤ n ≤ 5 (see docs/plan-low-degrees.md) instead bounds each factor by a + (1-a²)t and integrates a quartic. Neither may be folded into the other, so (⋆) is stated on its own.

Note that no division occurs anywhere: splitting the blog post's quotient ∏(1-azⱼ)/(a-zⱼ) into its numerator and denominator identities is what makes that possible, and p'(a) ≠ 0 is never needed.

Main statements

• Sendov.norm_sub_le_norm_one_sub_mul: the Möbius estimate;
• Sendov.one_le_integral_prod_norm: the branch point (⋆).

The Möbius estimate

theorem Sendov.norm_sub_le_norm_one_sub_mul {a : ℝ} (ha : |a| ≤ 1) {z : ℂ} (hz : ‖z‖ ≤ 1) : ‖↑a - z‖ ≤ ‖1 - ↑a * z‖

|a - z| ≤ |1 - a z| for real a with |a| ≤ 1 and z in the closed unit disk. The difference of squares is (1-a²)(1-|z|²), which is why a must be real: for complex a the cross terms contribute (conj a - a)(z - conj z), which need not vanish.

Products of norms over a multiset

theorem Sendov.norm_multiset_prod (s : Multiset ℂ) : ‖s.prod‖ = (Multiset.map (fun (w : ℂ) => ‖w‖) s).prod

theorem Sendov.prod_map_le_of_le {s : Multiset ℂ} {f g : ℂ → ℂ} (h : ∀ w ∈ s, ‖f w‖ ≤ ‖g w‖) : (Multiset.map (fun (w : ℂ) => ‖f w‖) s).prod ≤ (Multiset.map (fun (w : ℂ) => ‖g w‖) s).prod

The branch point

theorem Sendov.norm_prod_map (s : Multiset ℂ) (f : ℂ → ℂ) : ‖(Multiset.map f s).prod‖ = (Multiset.map (fun (w : ℂ) => ‖f w‖) s).prod

Norms distribute over a mapped multiset product.

theorem Sendov.prod_map_norm_nonneg (s : Multiset ℂ) (f : ℂ → ℂ) : 0 ≤ (Multiset.map (fun (w : ℂ) => ‖f w‖) s).prod

theorem Sendov.one_le_integral_prod_norm {n : ℕ} (hn : 2 ≤ n) {a : ℝ} (ha : |a| ≤ 1) {z q : Multiset ℂ} (hz : ∀ w ∈ z, ‖w‖ ≤ 1) (hpolar : 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) (hdenom : q.prod * (Multiset.map (fun (w : ℂ) => ↑a - w) z).prod = ↑n) : 1 ≤ ∫ (t : ℝ) in 0..1, (Multiset.map (fun (v : ℂ) => ‖↑a + ↑t * (1 - ↑a ^ 2) * v‖) q).prod

The branch point (⋆). 1 ≤ ∫₀¹ ∏ⱼ |a + t(1-a²)qⱼ| dt.

The high-degree argument relaxes this by AM–GM to the raw polar inequality; the low-degree argument bounds each factor by a + (1-a²)t. It is stated separately so that neither route has to reproduce the other's work.

The AM–GM relaxation to (1Q)

theorem Sendov.norm_sq_add_real_mul (a s : ℝ) (v : ℂ) : ‖↑a + ↑s * v‖ ^ 2 = a ^ 2 + 2 * a * s * v.re + s ^ 2 * ‖v‖ ^ 2

‖a + s v‖² = a² + 2 a s Re v + s² ‖v‖² for real a, s.

theorem Sendov.prod_map_sq (s : Multiset ℂ) (f : ℂ → ℝ) : (Multiset.map (fun (v : ℂ) => f v ^ 2) s).prod = (Multiset.map f s).prod ^ 2

theorem Sendov.sum_norm_sq_split (a s : ℝ) (q : Multiset ℂ) : (Multiset.map (fun (v : ℂ) => ‖↑a + ↑s * v‖ ^ 2) q).sum = ↑q.card * a ^ 2 + 2 * a * s * (Multiset.map (fun (v : ℂ) => v.re) q).sum + s ^ 2 * (Multiset.map (fun (v : ℂ) => ‖v‖ ^ 2) q).sum

Splitting ∑ⱼ ‖a + s qⱼ‖² into its three pieces.

theorem Sendov.sum_norm_sq_le_card (q : Multiset ℂ) (hq1 : ∀ v ∈ q, ‖v‖ ≤ 1) : (Multiset.map (fun (v : ℂ) => ‖v‖ ^ 2) q).sum ≤ ↑q.card

theorem Sendov.continuous_prod_norm (a : ℝ) (q : Multiset ℂ) : Continuous fun (t : ℝ) => (Multiset.map (fun (v : ℂ) => ‖↑a + ↑t * (1 - ↑a ^ 2) * v‖) q).prod

theorem Sendov.prod_norm_le_Ppolar {n : ℕ} (hn : 2 ≤ n) {a x t : ℝ} {q : Multiset ℂ} (hqcard : q.card = n - 1) (hq1 : ∀ v ∈ q, ‖v‖ ≤ 1) (hx : (Multiset.map (fun (v : ℂ) => v.re) q).sum = (↑n - 1) * x) : (Multiset.map (fun (v : ℂ) => ‖↑a + ↑t * (1 - ↑a ^ 2) * v‖) q).prod ≤ Ppolar a x t ^ ((↑n - 1) / 2)

The pointwise quadratic-mean bound. ∏ⱼ |a + t(1-a²)qⱼ| ≤ P(t)^{(n-1)/2)}, by AM–GM on the squares followed by ∑ ‖qⱼ‖² ≤ n-1.

theorem Sendov.one_le_integral_Ppolar {n : ℕ} (hn : 2 ≤ n) {a x : ℝ} {q : Multiset ℂ} (hqcard : q.card = n - 1) (hq1 : ∀ v ∈ q, ‖v‖ ≤ 1) (hx : (Multiset.map (fun (v : ℂ) => v.re) q).sum = (↑n - 1) * x) (hstar : 1 ≤ ∫ (t : ℝ) in 0..1, (Multiset.map (fun (v : ℂ) => ‖↑a + ↑t * (1 - ↑a ^ 2) * v‖) q).prod) : 1 ≤ ∫ (t : ℝ) in 0..1, Ppolar a x t ^ ((↑n - 1) / 2)

The raw polar inequality (1Q).