structure Polynomial.PosLogConcave (A : Polynomial ℝ) : Prop

A real polynomial is positively log-concave when all of its coefficients up to its degree are strictly positive and the coefficient sequence is logarithmically concave (aᵢ · aᵢ₊₂ ≤ aᵢ₊₁² for all i). Out-of-range coefficients are 0, which makes the log-concavity condition hold automatically outside the support.

• pos (i : ℕ) : i ≤ A.natDegree → 0 < A.coeff i

  Every coefficient up to the degree is strictly positive.

• lc (i : ℕ) : A.coeff i * A.coeff (i + 2) ≤ A.coeff (i + 1) ^ 2

  The coefficient sequence is logarithmically concave.

theorem Polynomial.PosLogConcave.coeff_nonneg {A : Polynomial ℝ} (hA : A.PosLogConcave) (i : ℕ) : 0 ≤ A.coeff i

theorem Polynomial.PosLogConcave.coeff_succ_eq_zero {A : Polynomial ℝ} (hA : A.PosLogConcave) {i : ℕ} (h : A.coeff i = 0) : A.coeff (i + 1) = 0

If a coefficient vanishes then so does the next one: PosLogConcave sequences have no internal zeros.

theorem Polynomial.PosLogConcave.ne_zero {A : Polynomial ℝ} (hA : A.PosLogConcave) : A ≠ 0

theorem Polynomial.PosLogConcave.genLC {A : Polynomial ℝ} (hA : A.PosLogConcave) (i j : ℕ) : i ≤ j → A.coeff i * A.coeff (j + 1) ≤ A.coeff (i + 1) * A.coeff j

Generalised log-concavity. For a PosLogConcave sequence the "spread" product aᵢ · aⱼ₊₁ is dominated by the "central" product aᵢ₊₁ · aⱼ whenever i ≤ j. This is the monotone-ratio consequence of log-concavity, formulated so that all indices stay in ℕ.

theorem Polynomial.PosLogConcave.mul_X_add_C {A : Polynomial ℝ} (hA : A.PosLogConcave) {r : ℝ} (hr : 0 < r) : ((X + C r) * A).PosLogConcave

Multiplying a PosLogConcave polynomial by a positive linear factor X + C r (0 < r) preserves PosLogConcave.

theorem Polynomial.PosLogConcave.mul_quadratic {A : Polynomial ℝ} (hA : A.PosLogConcave) {b c : ℝ} (hb : 0 < b) (hc : 0 < c) (hbc : c ≤ b ^ 2) : ((X ^ 2 + C b * X + C c) * A).PosLogConcave

Multiplying a PosLogConcave polynomial by a sector quadratic X² + C b * X + C c (0 < b, 0 < c, c ≤ b²) preserves PosLogConcave.

This is the hard kernel of the argument: a special case of Hoggar's 1974 theorem. The log-concavity of the product is certified by the exact identity dᵢ² − dᵢ₋₁·dᵢ₊₁ = c²·L(i-1) + bc·G₂ + b·G₃ + L₄ + c·G₅ + (b²−c)·L(i-2), in which each block is a nonnegative instance of log-concavity (lc) or generalised log-concavity (genLC) of A and every scalar coefficient is nonnegative because 0 < b, 0 < c, and c ≤ b².

def Polynomial.sector : Set ℂ

The closed Obreshkoff sector {z | z.re ≤ -‖z‖ / 2}: the closed sector of half-angle π/3 opening along the negative real axis. Note 0 ∈ sector.

Equations

• Polynomial.sector = {z : ℂ | z.re ≤ -‖z‖ / 2}

theorem Polynomial.mem_sector {z : ℂ} : z ∈ sector ↔ z.re ≤ -‖z‖ / 2

theorem Polynomial.ofReal_mem_sector {t : ℝ} : ↑t ∈ sector ↔ t ≤ 0

A real number lies in the sector (as a complex number) iff it is ≤ 0.

theorem Polynomial.conj_mem_sector {z : ℂ} (hz : z ∈ sector) : (starRingEnd ℂ) z ∈ sector

The sector is closed under complex conjugation.

theorem Polynomial.posLogConcave_of_aeval_mem_sector {Q : Polynomial ℝ} (hQ : Q.Monic) (h0 : Q.coeff 0 ≠ 0) (hroots : ∀ (z : ℂ), (aeval z) Q = 0 → z ∈ sector) : Q.PosLogConcave

sector core. If Q is monic with Q.coeff 0 ≠ 0 and every complex root of Q lies in the sector, then Q is positively log-concave.

theorem Polynomial.signVariations_eq_zero_of_coeff_nonneg {P : Polynomial ℝ} (h : ∀ (i : ℕ), 0 ≤ P.coeff i) : P.signVariations = 0

A nonnegative-coefficient polynomial has no sign variations.

theorem Polynomial.signVariations_le_one_of_coeff_threshold {P : Polynomial ℝ} {θ : ℕ} (h1 : ∀ i < θ, P.coeff i ≤ 0) (h2 : ∀ (i : ℕ), θ ≤ i → 0 ≤ P.coeff i) : P.signVariations ≤ 1

The threshold bound. If the coefficients of P are nonpositive below an index θ and nonnegative from θ on, then P has at most one sign variation.

theorem Polynomial.PosLogConcave.signVariations_X_pow_mul {A : Polynomial ℝ} (hQ : A.PosLogConcave) (k : ℕ) : (X ^ k * A).signVariations = 0

A PosLogConcave polynomial times any power of X has no sign variations.

theorem Polynomial.PosLogConcave.signVariations_X_pow_mul_X_sub_C_mul {A : Polynomial ℝ} (hA : A.PosLogConcave) (r : ℝ) (k : ℕ) : (X ^ k * ((X - C r) * A)).signVariations ≤ 1

The peeled threshold bound. Multiplying a PosLogConcave polynomial by one real linear factor X - C r (any r : ℝ) and any power of X yields at most one sign variation. For r ≤ 0 all coefficients stay nonnegative; for 0 < r the monotone-ratio consequence of log-concavity produces a single nonpositive-to-nonnegative threshold in the coefficients.

@[instance_reducible]

noncomputable instance Polynomial.instDecidablePredComplexMemSetSector : DecidablePred fun (x : ℂ) => x ∈ sector

Equations

• Polynomial.instDecidablePredComplexMemSetSector x✝ = decidable_of_iff (x✝.re ≤ -‖x✝‖ / 2) ⋯

theorem Polynomial.signVariations_le_one_of_sector {P : Polynomial ℝ} (hP : P ≠ 0) (h : Multiset.countP (fun (x : ℂ) => x ∉ sector) (map (algebraMap ℝ ℂ) P).roots ≤ 1) : P.signVariations ≤ 1

The sector variation bound (the core of the Obreshkoff two-circle theorem). If at most one complex root of the nonzero real polynomial P, counted with multiplicity, lies outside the sector {z | z.re ≤ -‖z‖ / 2}, then the coefficients of P have at most one sign variation.

theorem Polynomial.signVariations_eq_zero_of_sector {P : Polynomial ℝ} (hP : P ≠ 0) (h : Multiset.countP (fun (x : ℂ) => x ∉ sector) (map (algebraMap ℝ ℂ) P).roots = 0) : P.signVariations = 0

The λ = 0 case of the sector variation bound. If every complex root of the nonzero real polynomial P lies in the sector, its coefficients have no sign variation at all.