The $k$th $r$-Veronese section of a polynomial keeps the coefficients whose indices are congruent to $k$ modulo $r$. Every Veronese section of a nonzero real-rooted polynomial with nonnegative coefficients is zero or real-rooted. This follows from the Pólya frequency characterization and total nonnegativity.
Veronese section
def veroneseSectionPolynomial (r k : ℕ) (p : ℝ[X]) : ℝ[X] :=
if hr0 : r = 0 then 0 else
Polynomial.ofFinsupp <|
⟨Finsupp.onFinset (Finset.range (p.natDegree + 1))
(fun n => p.coeff (k + r * n))
(by
intro n hn
have hrpos : 0 < r := Nat.pos_of_ne_zero hr0
by_contra hmem
have hnotlt : ¬ n < p.natDegree + 1 := by simp_all
have hle : p.natDegree + 1 ≤ n := Nat.le_of_not_gt hnotlt
have hpn : p.natDegree < n := Nat.lt_of_succ_le hle
have hn_le_mul : n ≤ r * n := by
simpa [one_mul] using
Nat.mul_le_mul_right n (Nat.succ_le_of_lt hrpos)
have hn_le : n ≤ k + r * n :=
Nat.le_trans hn_le_mul (Nat.le_add_left (r * n) k)
exact hn <|
Polynomial.coeff_eq_zero_of_natDegree_lt (lt_of_lt_of_le hpn hn_le))⟩Veronese sections preserve real-rootedness
theorem preserve_realRooted_nonneg :
∀ {r k : ℕ}, 0 < r → k < r → {p : ℝ[X]} →
HasNonnegCoeffs p → p ≠ 0 → p.Splits →
veroneseSectionPolynomial r k p = 0 ∨
(veroneseSectionPolynomial r k p).SplitsLean source RealRooted/Challenges/VeroneseSections.lean at revision 5827550b.