Pólya frequency functions are closed under translation

Proved

DeBruijnNewman.pf_translate

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

analysisnumber-theory

Closure of Pólya frequency functions under translation (Schoenberg 1947): if K is a Pólya frequency function then so is x ↦ K(x − c) for every shift c. Proof: the minor entries K((x_i − c) − y_j) equal K(x_i − (y_j + c)), and shifting the y-nodes preserves strict increase, so the minor is a minor of K. Black-box role: recentering kernels (e.g. symmetrization arguments in de Bruijn's 1950 base case) stays inside 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_translate
    (K : ℝ → ℝ) (c : ℝ)
    (hK : IsPolyaFrequency K) :
    IsPolyaFrequency (fun x => K (x - c)) := 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