Pólya frequency functions are closed under nonnegative scalar multiples

Proved

DeBruijnNewman.pf_smul_nonneg

by junyihjy · Sep 23, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysisnumber-theory

Closure of Pólya frequency functions under nonnegative scalar multiples (I. J. Schoenberg, 1947, "On totally positive functions, distributions and Fourier transforms"): if K is a Pólya frequency function and a ≥ 0, then x ↦ a·K(x) is a Pólya frequency function. The proof is one determinant computation: the minor of the scaled kernel is a^n times the minor of K (Matrix.det_smul), hence nonnegative. Black-box role: lets later assembly scale PF kernels (e.g. normalizing the de Bruijn kernel) without leaving the PF class.

Preamble

import Mathlib

namespace DeBruijnNewman

/-- A function `K : ℝ → ℝ` is a Pólya frequency function if the translation
kernel `(x, y) ↦ K (x - y)` is totally positive of every order: every
finite minor formed on strictly increasing nodes is nonnegative. -/
def IsPolyaFrequency (K : ℝ → ℝ) : Prop :=
  ∀ (n : ℕ) (x y : Fin n → ℝ),
    (∀ i j : Fin n, i < j → x i < x j) →
    (∀ i j : Fin n, i < j → y i < y j) →
    0 ≤ (Matrix.of fun i j => K (x i - y j)).det

end DeBruijnNewman

Formal statement

namespace DeBruijnNewman

theorem pf_smul_nonneg
    (K : ℝ → ℝ) (a : ℝ) (ha : 0 ≤ a)
    (hK : IsPolyaFrequency K) :
    IsPolyaFrequency (fun x => a * K x) := by
  sorry

end DeBruijnNewman

Source

Decomposition of DeBruijnNewman.schoenberg_polya_fourier_real_zeros (626a294b-1b0a-43b9-aebe-aef9f7c9a57a), Prove2Me The de Bruijn-Newman Constant is Non-negative mission

View graph