The defect lemma

For points w₁, …, w_N in the closed unit disk,

(∏ ‖wⱼ‖) · ∑ⱼ ‖wⱼ⁻¹ - conj wⱼ‖ ≤ 1 - (∏ ‖wⱼ‖)².

The origin argument uses this to replace the inversion identities 1/zⱼ = conj zⱼ, which hold only when the points lie on the unit circle, by inequalities valid throughout the disk, at a cost proportional to 1 - |J|² where J is the product.

The blog post proves it by writing ‖wⱼ‖ = e^{-aⱼ}, computing ‖wⱼ⁻¹ - conj wⱼ‖ = 2 sinh aⱼ, and reducing to superadditivity of sinh. None of that is needed. Splitting off one point,

D (w ::ₘ t) = P · (r · δ_w) + r · D t, r = ‖w‖, P = ∏ over t,

the pointwise fact r · δ_w ≤ 1 - r² and the inductive hypothesis D t ≤ 1 - P² leave

1 - r²P² - [P(1-r²) + r(1-P²)] = (1-r)(1-P)(1-rP) ≥ 0,

which is immediate for r, P ∈ [0,1].

Points at the origin need no separate treatment. There wⱼ⁻¹ is Lean's junk value 0, but the pointwise fact is still true — as an inequality rather than an equality — because the left-hand side carries a factor ‖wⱼ‖. A limiting argument, which the informal proof needs, is therefore avoided.

Main statements

• Sendov.norm_mul_norm_inv_sub_conj_le: the pointwise fact;
• Sendov.defect: the lemma.

Products of norms

theorem Sendov.prod_norm_nonneg (s : Multiset ℂ) : 0 ≤ (Multiset.map (fun (z : ℂ) => ‖z‖) s).prod

theorem Sendov.prod_norm_le_one (s : Multiset ℂ) : (∀ z ∈ s, ‖z‖ ≤ 1) → (Multiset.map (fun (z : ℂ) => ‖z‖) s).prod ≤ 1

The pointwise fact

theorem Sendov.norm_mul_norm_inv_sub_conj_le {w : ℂ} (hw : ‖w‖ ≤ 1) : ‖w‖ * ‖w⁻¹ - (starRingEnd ℂ) w‖ ≤ 1 - ‖w‖ ^ 2

‖w‖ · ‖w⁻¹ - conj w‖ ≤ 1 - ‖w‖² for ‖w‖ ≤ 1, with equality unless w = 0. The factor ‖w‖ on the left is what makes the origin harmless.

The lemma

theorem Sendov.defect (s : Multiset ℂ) : (∀ z ∈ s, ‖z‖ ≤ 1) → (Multiset.map (fun (z : ℂ) => ‖z‖) s).prod * (Multiset.map (fun (z : ℂ) => ‖z⁻¹ - (starRingEnd ℂ) z‖) s).sum ≤ 1 - (Multiset.map (fun (z : ℂ) => ‖z‖) s).prod ^ 2

The defect lemma.