noncomputable def HexRootsMathlib.remotePoly (s : Multiset ℂ) : Polynomial ℂ

The normalized product with inverse-root parameters.

Equations

• HexRootsMathlib.remotePoly s = (Multiset.map (fun (a : ℂ) => 1 - Polynomial.C a * Polynomial.X) s).prod

theorem HexRootsMathlib.coeff_remotePoly (s : Multiset ℂ) (k : ℕ) : (remotePoly s).coeff k = (-1) ^ k * s.esymm k

Coefficients of the normalized remote-root product are the elementary symmetric functions of its parameters, with alternating sign.

theorem HexRootsMathlib.remotePoly_tail_le {s : Multiset ℂ} {d ρ : ℝ} (hd : 0 < d) (hρ : 0 ≤ ρ) (hs : ∀ z ∈ s, d ≤ ‖z‖) : ∑ k ∈ (Finset.range (s.card + 1)).erase 0, ‖(remotePoly (Multiset.map Inv.inv s)).coeff k‖ * ρ ^ k ≤ (1 + ρ / d) ^ s.card - 1

The item-25 bound is exactly a coefficient-tail bound for the normalized remote-root product.

@[simp]

theorem HexRootsMathlib.coeff_remotePoly_zero (s : Multiset ℂ) : (remotePoly s).coeff 0 = 1

The normalized remote-root product has constant coefficient one.

theorem HexRootsMathlib.natDegree_remotePoly_le (s : Multiset ℂ) : (remotePoly s).natDegree ≤ s.card

The normalized product has degree at most the number of parameters, including when a zero parameter makes a nominal linear factor constant.

theorem HexRootsMathlib.normalize_root_product (s : Multiset ℂ) (hs : ∀ z ∈ s, z ≠ 0) : Polynomial.C (Multiset.map Neg.neg s).prod * remotePoly (Multiset.map Inv.inv s) = (Multiset.map (fun (z : ℂ) => Polynomial.X - Polynomial.C z) s).prod

Normalizing each nonzero linear root factor by its constant term produces the inverse-root polynomial remotePoly.

theorem HexRootsMathlib.C_coeff_zero_mul_remotePoly (p : Polynomial ℂ) (hp : p ≠ 0) (h0 : p.coeff 0 ≠ 0) : Polynomial.C (p.coeff 0) * remotePoly (Multiset.map Inv.inv p.roots) = p

A nonzero complex polynomial with nonzero constant term is its constant term times the normalized inverse-root product. This is the polynomial bridge from item 25's multiset estimate.

noncomputable def HexRootsMathlib.coeffMass (p : Polynomial ℂ) (n : ℕ) (ρ : ℝ) : ℝ

The weighted coefficient mass through degree < n.

Equations

• HexRootsMathlib.coeffMass p n ρ = ∑ k ∈ Finset.range n, ‖p.coeff k‖ * ρ ^ k

theorem HexRootsMathlib.coeffMass_X_sub_C_mul_le {g : Polynomial ℂ} {a : ℂ} {n : ℕ} {ρ : ℝ} (hρ : 0 ≤ ρ) (hdeg : g.natDegree < n) : coeffMass ((Polynomial.X - Polynomial.C a) * g) (n + 1) ρ ≤ (ρ + ‖a‖) * coeffMass g n ρ

Multiplication by one linear factor increases weighted coefficient mass by at most the weighted mass of that factor.

theorem HexRootsMathlib.coeffMass_remotePoly_le {s : Multiset ℂ} {d ρ : ℝ} (hd : 0 < d) (hρ : 0 ≤ ρ) (hs : ∀ z ∈ s, d ≤ ‖z‖) : coeffMass (remotePoly (Multiset.map Inv.inv s)) (s.card + 1) ρ ≤ (1 + ρ / d) ^ s.card

Item 25 bounds the entire weighted mass of the normalized remote polynomial after restoring its constant coefficient.

theorem HexRootsMathlib.coeff_one_remotePoly_le {s : Multiset ℂ} {d ρ : ℝ} (hd : 0 < d) (hρ : 0 ≤ ρ) (hs : ∀ z ∈ s, d ≤ ‖z‖) : ‖(remotePoly (Multiset.map Inv.inv s)).coeff 1‖ * ρ ≤ (1 + ρ / d) ^ s.card - 1

The first remote coefficient is bounded by the same positive-degree tail. This also covers the degree-one case, where the remote multiset is empty and the coefficient vanishes.

theorem HexRootsMathlib.natDegree_eq_of_roots {q : Polynomial ℂ} {a : ℂ} {s : Multiset ℂ} (hroots : q.roots = a ::ₘ s) : q.natDegree = s.card + 1

The degree side condition paired with pellet_one_of_roots. Keeping it next to the dominance theorem makes the two hypotheses of pellet directly available from the same root-multiset decomposition.

theorem HexRootsMathlib.pellet_one_of_roots {q : Polynomial ℂ} {a : ℂ} {s : Multiset ℂ} {d ρ : ℝ} (hq : q ≠ 0) (hroots : q.roots = a ::ₘ s) (hd : 0 < d) (hρ : 0 ≤ ρ) (hremote : ∀ z ∈ s, d ≤ ‖z‖) (hmargin : ‖a‖ + (ρ + 3 * ‖a‖) * ((1 + ρ / d) ^ s.card - 1) < ρ) : ∑ i ∈ (Finset.range (s.card + 2)).erase 1, ‖q.coeff i‖ * ρ ^ i < ‖q.coeff 1‖ * ρ ^ 1

Exact first-term Pellet converse. Suppose the complete root multiset of q consists of one designated near root a and the remote multiset s. If every remote root is at least d from zero and the displayed wide-margin inequality holds, then the first coefficient of q strictly dominates the complete coefficient tail at radius ρ.

The exponent s.card counts remote roots with multiplicity. The statement also covers s = 0, so linear polynomials require no separate API.

theorem HexRootsMathlib.pellet_one_comp_dominates {p : Polynomial ℂ} {c z : ℂ} {s : Multiset ℂ} {d ρ : ℝ} (hp : p ≠ 0) (hroots : p.roots = z ::ₘ s) (hd : 0 < d) (hρ : 0 ≤ ρ) (hremote : ∀ w ∈ s, d ≤ ‖w - c‖) (hmargin : ‖z - c‖ + (ρ + 3 * ‖z - c‖) * ((1 + ρ / d) ^ s.card - 1) < ρ) : ∑ i ∈ (Finset.range (s.card + 2)).erase 1, ‖(p.comp (Polynomial.X + Polynomial.C c)).coeff i‖ * ρ ^ i < ‖(p.comp (Polynomial.X + Polynomial.C c)).coeff 1‖ * ρ ^ 1

Translation form of pellet_one_of_roots. Here z is the designated root of p, s is the multiset of every other root (with multiplicity), and the conclusion is stated directly for the Taylor polynomial about an arbitrary centre c.

This is the clean-margin terminus of the Pellet converse; the executable completeness chain in Completeness.PelletDyadic uses the slack variant pellet_one_comp_slack instead, which absorbs the dyadic rounding gap.