noncomputable def Polynomial.robinsonFactor (α : ℂ) : Polynomial ℂ

The linear factor contributed by a root in the Robinson form.

Equations

• Polynomial.robinsonFactor α = if ‖α‖ ≤ 1 then Polynomial.X - Polynomial.C α else 1 - Polynomial.C ((starRingEnd ℂ) α) * Polynomial.X

noncomputable def Polynomial.robinsonForm (p : Polynomial ℂ) : Polynomial ℂ

The Robinson form of a complex polynomial, obtained by Schur-reflecting roots outside the closed unit disk.

Equations

• p.robinsonForm = Polynomial.C p.leadingCoeff * (Multiset.map Polynomial.robinsonFactor p.roots).prod

noncomputable def Polynomial.schurReflectedRoot (α : ℂ) : ℂ

The root obtained by Schur-reflecting α across the unit circle.

Equations

• Polynomial.schurReflectedRoot α = ((starRingEnd ℂ) α)⁻¹

noncomputable def Polynomial.schurRootPath (α : ℂ) (t : ℝ) : ℂ

The straight-line root path from α to its Schur reflection. The Boyd/Mahler single-factor argument needs a monotonicity theorem for the Mahler measure of the derivative along this family.

Equations

• Polynomial.schurRootPath α t = ↑(1 - t) * α + ↑t * Polynomial.schurReflectedRoot α

noncomputable def Polynomial.derivativeMahlerAlongLinearFactor (f : Polynomial ℂ) (β : ℂ) : ℝ

Mahler measure of the derivative after adjoining one moving linear factor.

Equations

• f.derivativeMahlerAlongLinearFactor β = (Polynomial.derivative (f * (Polynomial.X - Polynomial.C β))).mahlerMeasure

noncomputable def Polynomial.schurReflectedAtRootForm (p : Polynomial ℂ) (α : ℂ) : Polynomial ℂ

The polynomial obtained from p by Schur-reflecting one selected exterior root while leaving all other roots in their original linear factors.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Polynomial.rootDeletionDerivativeSummand (p : Polynomial ℂ) (α : ℂ) : Polynomial ℂ

The summand obtained by differentiating the linear factor for one root.

Equations

• p.rootDeletionDerivativeSummand α = Polynomial.C p.leadingCoeff * (Multiset.map (fun (β : ℂ) => Polynomial.X - Polynomial.C β) (p.roots.erase α)).prod

theorem Polynomial.derivative_eq_sum_rootDeletionDerivativeSummand (p : Polynomial ℂ) : derivative p = (Multiset.map (fun (α : ℂ) => p.rootDeletionDerivativeSummand α) p.roots).sum

Leibniz expansion of the derivative over the splitting field: p.derivative is the sum, over the roots α of p, of the root-deletion summands rootDeletionDerivativeSummand p α. CLDColumnBound uses this to bound each derivative coefficient through the individual summands.

theorem Polynomial.mahlerMeasure_rootDeletionDerivativeSummand_le (p : Polynomial ℂ) (α : ℂ) : (p.rootDeletionDerivativeSummand α).mahlerMeasure ≤ p.mahlerMeasure

Each root-deletion summand has Mahler measure at most that of p: deleting the linear factor X - C α from the full root product only drops the max 1 ‖·‖ weight of that root. This is the per-summand bound CLDColumnBound combines with the Leibniz expansion above.

@[simp]

theorem Polynomial.schurRootPath_zero (α : ℂ) : schurRootPath α 0 = α

The Schur root path starts at α (the t = 0 endpoint).

@[simp]

theorem Polynomial.schurRootPath_one (α : ℂ) : schurRootPath α 1 = schurReflectedRoot α

The Schur root path ends at the reflected root (the t = 1 endpoint).

theorem Polynomial.reflectedLinearFactor_eq_C_mul_X_sub_C_schurReflectedRoot {α : ℂ} (hα : α ≠ 0) : 1 - C ((starRingEnd ℂ) α) * X = C (-(starRingEnd ℂ) α) * (X - C (schurReflectedRoot α))

The reflected linear factor 1 - C (conj α) * X factors as C (-(conj α)) * (X - C (schurReflectedRoot α)), exhibiting schurReflectedRoot α as its single root with leading coefficient -(conj α).

theorem Polynomial.derivativeMahler_reflectedLinearFactor_eq (f : Polynomial ℂ) {α : ℂ} (hα : α ≠ 0) : (derivative (f * (1 - C ((starRingEnd ℂ) α) * X))).mahlerMeasure = ‖α‖ * f.derivativeMahlerAlongLinearFactor (schurReflectedRoot α)

Replacing the moving linear factor by its reflected form scales the derivative's Mahler measure by ‖α‖: the Mahler measure of (f * (1 - C (conj α) * X)).derivative equals ‖α‖ times derivativeMahlerAlongLinearFactor f (schurReflectedRoot α).

theorem Polynomial.derivativeMahlerAlongLinearFactor_le_schurReflectedRoot_of_monotoneOn (f : Polynomial ℂ) (α : ℂ) (hmono : MonotoneOn (fun (t : ℝ) => f.derivativeMahlerAlongLinearFactor (schurRootPath α t)) (Set.Icc 0 1)) : f.derivativeMahlerAlongLinearFactor α ≤ f.derivativeMahlerAlongLinearFactor (schurReflectedRoot α)

If the derivative Mahler measure is monotone along the Schur path on [0,1], its value at the original root α is at most its value at the reflected root; the comparison of the two path endpoints.

theorem Polynomial.mahlerMeasure_derivative_le_of_schurRootPath_monotone (f : Polynomial ℂ) {α : ℂ} (hα : 1 < ‖α‖) (hmono : f.derivativeMahlerAlongLinearFactor α ≤ f.derivativeMahlerAlongLinearFactor (schurReflectedRoot α)) : (derivative (f * (X - C α))).mahlerMeasure ≤ (derivative (f * (1 - C ((starRingEnd ℂ) α) * X))).mahlerMeasure

For an exterior root (1 < ‖α‖), assuming the derivative Mahler measure does not decrease from α to its reflection, replacing X - C α by the reflected factor 1 - C (conj α) * X does not decrease the derivative's Mahler measure.

theorem Polynomial.mahlerMeasure_derivative_le_of_schurRootPath_monotoneOn (f : Polynomial ℂ) {α : ℂ} (hα : 1 < ‖α‖) (hmono : MonotoneOn (fun (t : ℝ) => f.derivativeMahlerAlongLinearFactor (schurRootPath α t)) (Set.Icc 0 1)) : (derivative (f * (X - C α))).mahlerMeasure ≤ (derivative (f * (1 - C ((starRingEnd ℂ) α) * X))).mahlerMeasure

MonotoneOn-hypothesis form of mahlerMeasure_derivative_le_of_schurRootPath_monotone: the path-monotonicity premise is reduced to the endpoint comparison automatically.

theorem Polynomial.mahlerMeasure_derivative_le_schurReflectedAtRootForm_derivative_of_monotoneOn (p : Polynomial ℂ) {α : ℂ} (hαmem : α ∈ p.roots) (hα : 1 < ‖α‖) (hmono : MonotoneOn (fun (t : ℝ) => (C p.leadingCoeff * (Multiset.map (fun (β : ℂ) => X - C β) (p.roots.erase α)).prod).derivativeMahlerAlongLinearFactor (schurRootPath α t)) (Set.Icc 0 1)) : (derivative p).mahlerMeasure ≤ (derivative (p.schurReflectedAtRootForm α)).mahlerMeasure

One root-reflection step in the de Bruijn-Springer/Boyd method toward p.derivative.mahlerMeasure ≤ p.natDegree * p.mahlerMeasure: if the Mahler measure of the derivative is monotone along the Schur path for the selected linear factor, then reflecting that exterior root cannot decrease the Mahler measure of the derivative.

@[simp]

theorem Polynomial.robinsonFactor_of_norm_le {α : ℂ} (hα : ‖α‖ ≤ 1) : robinsonFactor α = X - C α

For a root in the closed unit disk, the Robinson factor is the ordinary X - C α.

@[simp]

theorem Polynomial.robinsonFactor_of_one_lt_norm {α : ℂ} (hα : 1 < ‖α‖) : robinsonFactor α = 1 - C ((starRingEnd ℂ) α) * X

For an exterior root, the Robinson factor is the reflected 1 - C (conj α) * X.

@[simp]

theorem Polynomial.robinsonForm_zero : robinsonForm 0 = 0

The Robinson form of the zero polynomial is zero.

theorem Polynomial.norm_eval_robinsonFactor_eq_norm_eval_X_sub_C {α z : ℂ} (hz : ‖z‖ = 1) : ‖eval z (robinsonFactor α)‖ = ‖eval z (X - C α)‖

On the unit circle (‖z‖ = 1) the Robinson factor has the same modulus as the unreflected factor X - C α. Schur reflection moves roots across the circle but preserves the boundary modulus pointwise.

theorem Polynomial.norm_eval_robinsonForm_eq_norm_eval {p : Polynomial ℂ} {z : ℂ} (hz : ‖z‖ = 1) : ‖eval z p.robinsonForm‖ = ‖eval z p‖

The Robinson form agrees with p in modulus everywhere on the unit circle; the pointwise boundary identity behind the Mahler-measure equality mahlerMeasure_robinsonForm.

theorem Polynomial.logMahlerMeasure_eq_of_boundary_norm_eq {p q : Polynomial ℂ} (hboundary : ∀ {z : ℂ}, ‖z‖ = 1 → ‖eval z q‖ = ‖eval z p‖) : q.logMahlerMeasure = p.logMahlerMeasure

Two polynomials with equal modulus everywhere on the unit circle have equal logarithmic Mahler measure, since the latter is the circle average of log ‖·‖.

theorem Polynomial.mahlerMeasure_eq_of_boundary_norm_eq_of_ne_zero {p q : Polynomial ℂ} (hboundary : ∀ {z : ℂ}, ‖z‖ = 1 → ‖eval z q‖ = ‖eval z p‖) (hp : p ≠ 0) (hq : q ≠ 0) : q.mahlerMeasure = p.mahlerMeasure

Nonzero polynomials with equal modulus on the unit circle have equal Mahler measure (exponentiating logMahlerMeasure_eq_of_boundary_norm_eq).

theorem Polynomial.mahlerMeasure_le_circleAverage_norm (p : Polynomial ℂ) : p.mahlerMeasure ≤ Real.circleAverage (fun (z : ℂ) => ‖eval z p‖) 0 1

Jensen/circle-average upper bound used in the Mahler--Boyd analytic method: the exponential Mahler measure is bounded by the unit-circle mean of the absolute value. This is the first Jensen step in the standard Landau/Mahler integral proof, exposed here so derivative-bound arguments can cite the analytic ingredient directly rather than hiding it inside a coefficient norm estimate.

theorem Polynomial.mahlerMeasure_robinsonFactor (α : ℂ) : (robinsonFactor α).mahlerMeasure = max 1 ‖α‖

The Mahler measure of a single Robinson factor is max 1 ‖α‖.

theorem Polynomial.mahlerMeasure_robinsonForm (p : Polynomial ℂ) : p.robinsonForm.mahlerMeasure = p.mahlerMeasure

Schur reflection preserves the Mahler measure: p.robinsonForm and p have the same Mahler measure (the multiplicative form of the boundary-modulus identity).

theorem Polynomial.robinsonFactor_ne_zero (α : ℂ) : robinsonFactor α ≠ 0

Every Robinson factor is nonzero (it has degree one).

theorem Polynomial.norm_root_robinsonFactor_le (α : ℂ) {β : ℂ} (hβ : β ∈ (robinsonFactor α).roots) : ‖β‖ ≤ 1

Each root of a Robinson factor lies in the closed unit disk.

theorem Polynomial.norm_root_robinsonForm_le {p : Polynomial ℂ} {β : ℂ} (hβ : β ∈ p.robinsonForm.roots) : ‖β‖ ≤ 1

Every root of p.robinsonForm lies in the closed unit disk: this is the defining property of the Robinson form (exterior roots have been reflected inward).

theorem Polynomial.natDegree_robinsonFactor (α : ℂ) : (robinsonFactor α).natDegree = 1

Each Robinson factor has degree one.

theorem Polynomial.natDegree_robinsonForm (p : Polynomial ℂ) : p.robinsonForm.natDegree = p.natDegree

The Robinson form preserves the degree of p.

theorem Polynomial.norm_root_robinsonForm_derivative_le {p : Polynomial ℂ} {β : ℂ} (hβ : β ∈ (derivative p.robinsonForm).roots) : ‖β‖ ≤ 1

Every root of p.robinsonForm.derivative lies in the closed unit disk. By Gauss-Lucas the derivative's roots sit in the convex hull of the roots of p.robinsonForm, which is itself inside the closed unit disk.

theorem Polynomial.norm_root_derivative_le_of_roots_le_one {p : Polynomial ℂ} (hroots : ∀ α ∈ p.roots, ‖α‖ ≤ 1) {β : ℂ} (hβ : β ∈ (derivative p).roots) : ‖β‖ ≤ 1

Gauss-Lucas for the closed unit disk: if every root of p lies in the closed unit disk, so does every root of p.derivative.

theorem Polynomial.mahlerMeasure_derivative_eq_natDegree_mul_of_roots_le_one (p : Polynomial ℂ) (hroots : ∀ α ∈ p.roots, ‖α‖ ≤ 1) : (derivative p).mahlerMeasure = ↑p.natDegree * p.mahlerMeasure

For a polynomial with all roots in the closed unit disk, the derivative's Mahler measure is exactly natDegree * mahlerMeasure (both sides reduce to a leading coefficient norm, scaled by the degree).

theorem Polynomial.mahlerMeasure_derivative_map_intCast_le_of_roots_le_one (f : Polynomial ℤ) (hroots : ∀ α ∈ (map (Int.castRingHom ℂ) f).roots, ‖α‖ ≤ 1) : (map (Int.castRingHom ℂ) (derivative f)).mahlerMeasure ≤ ↑f.natDegree * (map (Int.castRingHom ℂ) f).mahlerMeasure

Integer-coefficient form: if the complexification of f : ℤ[X] has all roots in the closed unit disk, the Mahler measure of f.derivative's complexification is at most f.natDegree times that of f's.

theorem Polynomial.Multiset.prod_le_of_sum_log_le {s t : Multiset ℝ} (hs : ∀ x ∈ s, 0 < x) (ht : ∀ x ∈ t, 0 < x) (hlog : (Multiset.map (fun (x : ℝ) => Real.log x) s).sum ≤ (Multiset.map (fun (x : ℝ) => Real.log x) t).sum) : s.prod ≤ t.prod

For multisets of positive reals, a comparison of log-sums (∑ log ≤ ∑ log) lifts to a comparison of the products (∏ ≤ ∏).

theorem Polynomial.prod_max_one_norm_roots_derivative_le_of_sum_log_le (p : Polynomial ℂ) (hlog : (Multiset.map (fun (β : ℂ) => Real.log (max 1 ‖β‖)) (derivative p).roots).sum ≤ (Multiset.map (fun (α : ℂ) => Real.log (max 1 ‖α‖)) p.roots).sum) : (Multiset.map (fun (β : ℂ) => max 1 ‖β‖) (derivative p).roots).prod ≤ (Multiset.map (fun (α : ℂ) => max 1 ‖α‖) p.roots).prod

The max 1 ‖·‖ root-product comparison derivative ≤ original follows from the corresponding sum-of-logs comparison, via Multiset.prod_le_of_sum_log_le.

theorem Polynomial.prod_max_one_norm_roots_derivative_le_of_schmeisser_radius_one (p : Polynomial ℂ) (hSchmeisser : (Multiset.map (fun (β : ℂ) => ‖β‖) (Multiset.filter (fun (β : ℂ) => 1 ≤ ‖β‖) (derivative p).roots)).prod ≤ (Multiset.map (fun (α : ℂ) => ‖α‖) (Multiset.filter (fun (α : ℂ) => 1 ≤ ‖α‖) p.roots)).prod) : (Multiset.map (fun (β : ℂ) => max 1 ‖β‖) (derivative p).roots).prod ≤ (Multiset.map (fun (α : ℂ) => max 1 ‖α‖) p.roots).prod

The desired derivative root-product comparison follows from the r = 1 instance of Schmeisser's de Bruijn-Springer product inequality.

theorem Polynomial.roots_filter_norm_product_derivative_le_of_X_mul_derivative (p : Polynomial ℂ) (h : (Multiset.map (fun (β : ℂ) => ‖β‖) (Multiset.filter (fun (β : ℂ) => 1 ≤ ‖β‖) (X * derivative p).roots)).prod ≤ (Multiset.map (fun (α : ℂ) => ‖α‖) (Multiset.filter (fun (α : ℂ) => 1 ≤ ‖α‖) p.roots)).prod) : (Multiset.map (fun (β : ℂ) => ‖β‖) (Multiset.filter (fun (β : ℂ) => 1 ≤ ‖β‖) (derivative p).roots)).prod ≤ (Multiset.map (fun (α : ℂ) => ‖α‖) (Multiset.filter (fun (α : ℂ) => 1 ≤ ‖α‖) p.roots)).prod

The Schmeisser specialization is naturally applied to X * p.derivative. The extra root contributed by X is 0, hence it is removed by the 1 ≤ ‖β‖ filter.

theorem Polynomial.prod_max_one_norm_roots_derivative_le_of_mahlerMeasure_derivative_le (p : Polynomial ℂ) (hderiv : (derivative p).mahlerMeasure ≤ ↑p.natDegree * p.mahlerMeasure) : (Multiset.map (fun (β : ℂ) => max 1 ‖β‖) (derivative p).roots).prod ≤ (Multiset.map (fun (α : ℂ) => max 1 ‖α‖) p.roots).prod

A Mahler-measure derivative bound p.derivative.mahlerMeasure ≤ natDegree * p.mahlerMeasure implies the max 1 ‖·‖ root-product comparison between p.derivative and p, cancelling the common natDegree * ‖leadingCoeff‖ scale.

theorem Polynomial.prod_max_one_norm_roots_derivative_le_of_roots_le_one (p : Polynomial ℂ) (hroots : ∀ α ∈ p.roots, ‖α‖ ≤ 1) : (Multiset.map (fun (β : ℂ) => max 1 ‖β‖) (derivative p).roots).prod ≤ (Multiset.map (fun (α : ℂ) => max 1 ‖α‖) p.roots).prod

Closed-unit-disk derivative root-product comparison. The analytic input is Gauss-Lucas: derivative roots stay in the convex hull of the original roots, which is still contained in the closed unit disk.

theorem Polynomial.prod_max_one_norm_roots_robinsonForm_derivative_le (p : Polynomial ℂ) : (Multiset.map (fun (β : ℂ) => max 1 ‖β‖) (derivative p.robinsonForm).roots).prod ≤ (Multiset.map (fun (α : ℂ) => max 1 ‖α‖) p.roots).prod

Robinson endpoint root-product comparison for the derivative. This is the closed-disk endpoint of the de Bruijn-Springer/Boyd reflection method: all roots of p.robinsonForm lie in the closed unit disk, so Gauss-Lucas puts all roots of its derivative there as well.

theorem Polynomial.MahlerMeasure.derivative_le_of_boundary {p q : Polynomial ℂ} (hpderiv : (derivative p).mahlerMeasure ≤ ↑p.natDegree * p.mahlerMeasure) (hboundary : ∀ {z : ℂ}, ‖z‖ = 1 → ‖eval z q‖ = ‖eval z p‖) (hqroots : ∀ {β : ℂ}, β ∈ q.roots → ‖β‖ ≤ 1) (hdeg : q.natDegree = p.natDegree) : (derivative p).mahlerMeasure ≤ (derivative q).mahlerMeasure

Boyd boundary-comparison theorem. Boundary equality and the closed-disk root hypothesis for q identify the right side as q.natDegree * q.mahlerMeasure; the additional hypothesis hpderiv is the derivative Mahler bound needed on the source polynomial.

theorem Polynomial.mahlerMeasure_robinsonForm_derivative (p : Polynomial ℂ) : (derivative p.robinsonForm).mahlerMeasure = ↑p.natDegree * p.mahlerMeasure

The derivative of the Robinson form attains the exact identity mahlerMeasure = natDegree * mahlerMeasure, combining root-confinement (norm_root_robinsonForm_le) with degree and measure preservation.

theorem Polynomial.mahlerMeasure_robinsonRootDeletionDerivativeSum_le (p : Polynomial ℂ) : (C p.leadingCoeff * (Multiset.map (fun (α : ℂ) => (Multiset.map robinsonFactor (p.roots.erase α)).prod * derivative (robinsonFactor α)) p.roots).sum).mahlerMeasure ≤ ↑p.natDegree * p.mahlerMeasure

The finite root-deletion derivative sum for the Robinson form has the same Mahler bound as the derivative itself.