The origin inequality #

This file closes the origin channel, deriving (origin-exact) — the hypothesis horigin of Sendov.polar_origin_incompatible — from the triangle inequality (tri) of Sendov.Analytic.Origin, the two origin identities, and the defect estimate of Sendov.Analytic.Jsum.

The chain is:

(f1aq) The two origin identities express F(1) + (n-1) a (x+iy) ∫₀¹F exactly, in terms of J = (∏ qⱼ)(∏ zⱼ) and ∑ⱼ 1/zⱼ. Feeding in Jsum_estimate collapses this to J·W/n plus an error of size a(1-|J|²)/(n-1), where W = a²(n-1) + 1 - a(x+iy).
(grow) ‖W‖ ≥ 2an/(n-1), which makes |J|·‖W‖/n + a(1-|J|²)/(n-1) non-decreasing in |J| on [0,1], so |J| may be replaced by 1. This reduces to the quadratic (n-1)²a² - (3n-1)a + (n-1) > 0, whose discriminant (3n-1)² - 4(n-1)³ is negative exactly from n ≥ 5 on. This is the only place the hypothesis n ≥ 5 is used.
Eliminating y. |s + it| ≤ s + t²/(2s) for s > 0, applied to W, whose real part a²(n-1) + 1 - ax is at least a²(n-1), and whose imaginary part is -ay with y² ≤ 1 - x².

Main statements #

Sendov.origin_exact: (origin-exact), in exactly the form polar_origin_incompatible wants;
Sendov.grow: the lower bound ‖W‖ ≥ 2an/(n-1).

Scalar lemmas #

source

theorem Sendov.sum_norm_le_card (q : Multiset ℂ) :

(∀ v ∈ q, ‖v‖ ≤ 1) → (Multiset.map (fun (v : ℂ) => ‖v‖) q).sum ≤ ↑q.card

source

theorem Sendov.norm_mul_two_re_le {w : ℂ} (_hs : 0 < w.re) :

‖w‖ * (2 * w.re) ≤ 2 * w.re ^ 2 + w.im ^ 2

|s + it| ≤ s + t²/(2s) for s > 0, in cleared form. Squaring both sides leaves t⁴ ≥ 0.

The quantity `W`, the growth bound `(grow)`, and the two real-arithmetic steps #

source

noncomputable def Sendov.Worigin (n : ℕ) (a x y : ℝ) :

ℂ

W = a²(n-1) + 1 - a(x+iy); n times the bracket in the blog post's (tri-2).

Equations

Sendov.Worigin n a x y = ↑a ^ 2 * (↑n - 1) + 1 - ↑a * (↑x + ↑y * Complex.I)

Instances For

source

theorem Sendov.Worigin_eq (n : ℕ) (a x y : ℝ) :

Worigin n a x y = ↑(a ^ 2 * (↑n - 1) + 1 - a * x) + ↑(-(a * y)) * Complex.I

source

theorem Sendov.Worigin_re (n : ℕ) (a x y : ℝ) :

(Worigin n a x y).re = a ^ 2 * (↑n - 1) + 1 - a * x

source

theorem Sendov.Worigin_im (n : ℕ) (a x y : ℝ) :

(Worigin n a x y).im = -(a * y)

source

theorem Sendov.grow {n : ℕ} (hn : 5 ≤ n) {a x y : ℝ} (ha0 : 0 < a) (hx : x ≤ 1) :

2 * a * ↑n / (↑n - 1) ≤ ‖Worigin n a x y‖

(grow). ‖W‖ ≥ 2an/(n-1). Bounding ‖W‖ below by its real part reduces this to (n-1)²a² - (3n-1)a + (n-1) > 0; completing the square turns that into 4(n-1)³ - (3n-1)² > 0, which is exactly where n ≥ 5 is needed.

source

theorem Sendov.collapse_J {K c P : ℝ} (hP1 : P ≤ 1) (hc0 : 0 ≤ c) (hcK : 2 * c ≤ K) :

P * K + c * (1 - P ^ 2) ≤ K

Replacing |J| by 1: P K + c(1 - P²) ≤ K on 0 ≤ P ≤ 1 once K ≥ 2c ≥ 0, since K - P K - c(1-P²) = (1-P)(K - c(1+P)).

source

theorem Sendov.norm_Worigin_le {n : ℕ} {a x y : ℝ} (ha0 : 0 < a) (ha1 : a < 1) (hn1 : 0 < ↑n - 1) (hxle : x ≤ 1) (hy2 : y ^ 2 ≤ 1 - x ^ 2) :

‖Worigin n a x y‖ ≤ a ^ 2 * (↑n - 1) + 1 - a * x + (1 - x ^ 2) / (2 * (↑n - 1))

Eliminating y: ‖W‖ ≤ Re W + (Im W)²/(2 Re W), then Re W ≥ a²(n-1) and y² ≤ 1 - x².

source

theorem Sendov.xy_bounds {n : ℕ} (hn : 2 ≤ n) {x y : ℝ} {q : Multiset ℂ} (hqcard : q.card = n - 1) (hq1 : ∀ v ∈ q, ‖v‖ ≤ 1) (hxy : q.sum = (↑n - 1) * (↑x + ↑y * Complex.I)) :

(Multiset.map (fun (v : ℂ) => v.re) q).sum = (↑n - 1) * x ∧ x ^ 2 + y ^ 2 ≤ 1

x and y are determined by q.sum, and inherit two bounds from ‖qⱼ‖ ≤ 1: the real part is what the polar and origin estimates need, and x² + y² ≤ 1 is what eliminates y.