The origin inequality: the pointwise estimate and (tri)

The origin argument controls F(t) = ∏ⱼ (1 - a t qⱼ) through its derivative,

F'(t) = -(n-1) a (x+iy) F(t) - a² t ∑ⱼ qⱼ² ∏_{k≠j} (1 - a t q_k),

whose error term is bounded by a² t (n-1) β(t)^{(n-2)/2}. Integrating that against the fundamental theorem of calculus and F(0) = 1 gives the triangle inequality (tri). The J-algebra that turns (tri) into (origin-exact) follows in a later file.

The error bound has three steps, in increasing order of depth:

• ∑ⱼ ‖1 - a t qⱼ‖² ≤ (n-1) β(t), the same expansion that produced the quadratic mean in the polar channel — this is where x enters;
• Cauchy–Schwarz, (∑ b)² ≤ N ∑ b²;
• Maclaurin's inequality, ∑ⱼ ∏_{k≠j} bₖ ≤ N (mean b)^{N-1} — the one ingredient absent from Mathlib, proved in Sendov.Analytic.Maclaurin.

The blog post applies Maclaurin to (1/(n-1)) ∑ⱼ ∏_{k≠j} |1 - a t q_k| and then Cauchy–Schwarz; the order is immaterial and it is done the same way here.

A note on the bookkeeping. The quantity ∑ⱼ ∏_{k≠j} f(qⱼ) is written as a sum over erasures of q, whereas Multiset.esymm — which Maclaurin is stated for — is a sum over sub-multisets of the image q.map f. Rather than relate erasure and map directly, which needs f injective, the two are matched through the recurrence they share.

Main statements

• Sendov.sumEraseProdMap_eq_esymm: the two forms of ∑ⱼ ∏_{k≠j} agree;
• Sendov.sum_norm_sq_one_sub_le: ∑ⱼ ‖1 - a t qⱼ‖² ≤ (n-1) β(t);
• Sendov.sumEraseProdMap_norm_le: the error bound (n-1) β(t)^{(n-2)/2};
• Sendov.hasDerivAt_Fprod: F'(t) = -a ∑ⱼ qⱼ ∏_{k≠j} (1 - a t q_k);
• Sendov.norm_deriv_add_le: ‖F'(t) + (n-1) a (x+iy) F(t)‖ ≤ a² t (n-1) β(t)^{(n-2)/2};
• Sendov.one_le_tri: the triangle inequality (tri).

The derivative is assembled from a weighted erasure sum sumEraseProdC q g f = ∑ⱼ g(qⱼ) ∏_{k≠j} f(q_k): taking g = id gives F' itself, and the identity 1 - (1 - a t qⱼ) = a t qⱼ splits that into the main term (∑ⱼ qⱼ) F(t) plus a t times the case g = (· ^ 2), which is the residual actually being estimated.

∑ⱼ ∏_{k≠j} over erasures, and esymm

noncomputable def Sendov.sumEraseProdMap {α : Type u_1} (s : Multiset α) (f : α → ℝ) : ℝ

∑ⱼ ∏_{k≠j} f(sₖ), as a sum over erasures of s.

Equations

• Sendov.sumEraseProdMap s f = (Multiset.map (fun (j : α) => (Multiset.map f (s.erase j)).prod) s).sum

theorem Sendov.sumEraseProdMap_cons {α : Type u_1} (v : α) (t : Multiset α) (f : α → ℝ) : sumEraseProdMap (v ::ₘ t) f = (Multiset.map f t).prod + f v * sumEraseProdMap t f

theorem Sendov.sumEraseProdMap_eq_esymm {α : Type u_1} (s : Multiset α) (f : α → ℝ) : s ≠ 0 → sumEraseProdMap s f = (Multiset.map f s).esymm ((Multiset.map f s).card - 1)

The erasure form and Multiset.esymm agree, matched through their common recurrence.

The quadratic mean

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

‖1 + s v‖² = 1 + 2 s Re v + s² ‖v‖² for real s.

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

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

∑ⱼ ‖1 - a t qⱼ‖² ≤ (n-1) β(t), where β(t) = 1 - 2 a x t + a² t².

Cauchy–Schwarz and the error bound

theorem Sendov.sq_sum_le_card_mul_sum_sq (s : Multiset ℝ) (hs : ∀ b ∈ s, 0 ≤ b) : s.sum ^ 2 ≤ ↑s.card * (Multiset.map (fun (b : ℝ) => b ^ 2) s).sum

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

The error bound. ∑ⱼ ∏_{k≠j} ‖1 - a t q_k‖ ≤ (n-1) β(t)^{(n-2)/2}: Maclaurin's inequality, then Cauchy–Schwarz, then the quadratic mean. Nonnegativity of β(t) is not assumed — it follows from the quadratic-mean bound, β(t) dominating an average of squares.

The derivative of F(t) = ∏ⱼ (1 - a t qⱼ)

noncomputable def Sendov.sumEraseProdC (s : Multiset ℂ) (g f : ℂ → ℂ) : ℂ

∑ⱼ g(qⱼ) ∏_{k≠j} f(q_k), the weighted erasure sum over ℂ. Taking g = id gives the derivative of a product; taking g = (· ^ 2) gives the residual left after the main term is split off.

Equations

• Sendov.sumEraseProdC s g f = (Multiset.map (fun (j : ℂ) => g j * (Multiset.map f (s.erase j)).prod) s).sum

@[simp]

theorem Sendov.sumEraseProdC_zero (g f : ℂ → ℂ) : sumEraseProdC 0 g f = 0

theorem Sendov.sumEraseProdC_cons (v : ℂ) (t : Multiset ℂ) (g f : ℂ → ℂ) : sumEraseProdC (v ::ₘ t) g f = g v * (Multiset.map f t).prod + f v * sumEraseProdC t g f

theorem Sendov.norm_sumEraseProdC_le (g f : ℂ → ℂ) (s : Multiset ℂ) : (∀ v ∈ s, ‖g v‖ ≤ 1) → ‖sumEraseProdC s g f‖ ≤ sumEraseProdMap s fun (v : ℂ) => ‖f v‖

A weighted erasure sum with unit-size weights is dominated by the unweighted one.

noncomputable def Sendov.Fprod (a : ℝ) (q : Multiset ℂ) (t : ℝ) : ℂ

F(t) = ∏ⱼ (1 - a t qⱼ).

Equations

• Sendov.Fprod a q t = (Multiset.map (fun (v : ℂ) => 1 - ↑a * ↑t * v) q).prod

@[simp]

theorem Sendov.Fprod_zero (a : ℝ) (q : Multiset ℂ) : Fprod a q 0 = 1

theorem Sendov.sumEraseProdC_id_eq (a t : ℝ) (q : Multiset ℂ) : (sumEraseProdC q id fun (v : ℂ) => 1 - ↑a * ↑t * v) = q.sum * Fprod a q t + ↑a * ↑t * sumEraseProdC q (fun (v : ℂ) => v ^ 2) fun (v : ℂ) => 1 - ↑a * ↑t * v

Splitting the derivative sum into its main term and its residual: ∑ⱼ qⱼ ∏_{k≠j}(1-atq_k) = (∑ⱼ qⱼ) F(t) + a t ∑ⱼ qⱼ² ∏_{k≠j}(1-atq_k), since 1 - (1 - a t qⱼ) = a t qⱼ.

theorem Sendov.hasDerivAt_Fprod (a t : ℝ) (q : Multiset ℂ) : HasDerivAt (Fprod a q) (-↑a * sumEraseProdC q id fun (v : ℂ) => 1 - ↑a * ↑t * v) t

F'(t) = -a ∑ⱼ qⱼ ∏_{k≠j}(1 - a t q_k).

theorem Sendov.norm_deriv_add_le {n : ℕ} (hn : 2 ≤ n) {a x y t : ℝ} {q : Multiset ℂ} (hqcard : q.card = n - 1) (hq0 : q ≠ 0) (hq1 : ∀ v ∈ q, ‖v‖ ≤ 1) (ha0 : 0 ≤ a) (ht0 : 0 ≤ t) (hx : (Multiset.map (fun (v : ℂ) => v.re) q).sum = (↑n - 1) * x) (hsum : q.sum = (↑↑n - 1) * (↑x + ↑y * Complex.I)) : ‖(-↑a * sumEraseProdC q id fun (v : ℂ) => 1 - ↑a * ↑t * v) + (↑↑n - 1) * ↑a * (↑x + ↑y * Complex.I) * Fprod a q t‖ ≤ a ^ 2 * t * (↑n - 1) * QQ (a * x) (a ^ 2) t ^ ((↑n - 2) / 2)

The pointwise estimate. ‖F'(t) + (n-1) a (x+iy) F(t)‖ ≤ a² t (n-1) β(t)^{(n-2)/2}.

Integrating the pointwise estimate: the triangle inequality (tri)

theorem Sendov.continuous_prodC (a : ℝ) (q : Multiset ℂ) : Continuous fun (t : ℝ) => (Multiset.map (fun (v : ℂ) => 1 - ↑a * ↑t * v) q).prod

theorem Sendov.continuous_Fprod (a : ℝ) (q : Multiset ℂ) : Continuous (Fprod a q)

theorem Sendov.continuous_sumEraseProdC (a : ℝ) (g : ℂ → ℂ) (q : Multiset ℂ) : Continuous fun (t : ℝ) => sumEraseProdC q g fun (v : ℂ) => 1 - ↑a * ↑t * v

theorem Sendov.one_le_tri {n : ℕ} (hn : 2 ≤ n) {a x y : ℝ} {q : Multiset ℂ} (hqcard : q.card = n - 1) (hq0 : q ≠ 0) (hq1 : ∀ v ∈ q, ‖v‖ ≤ 1) (ha0 : 0 ≤ a) (hx : (Multiset.map (fun (v : ℂ) => v.re) q).sum = (↑n - 1) * x) (hsum : q.sum = (↑n - 1) * (↑x + ↑y * Complex.I)) : 1 ≤ ‖Fprod a q 1 + (↑n - 1) * ↑a * (↑x + ↑y * Complex.I) * ∫ (t : ℝ) in 0..1, Fprod a q t‖ + a ^ 2 * (↑n - 1) * ∫ (t : ℝ) in 0..1, t * QQ (a * x) (a ^ 2) t ^ ((↑n - 2) / 2)

The triangle inequality (tri). Integrating norm_deriv_add_le against the fundamental theorem of calculus, using F(0) = 1.