Zeros of exponential polynomials

A real exponential polynomial is a function f(x) = ∑ₖ pₖ(x) exp(γₖ x) with real polynomials pₖ and real exponents γₖ, indexed by a finite set. If the index set is nonempty, the exponents are pairwise distinct and the pₖ are nonzero, then f has fewer than ∑ₖ (deg pₖ + 1) real zeros (TauCeti.card_lt_of_sum_eval_mul_exp_eq_zero); in particular its zero set is finite. Nonemptiness is needed: the empty sum vanishes everywhere. For a single term this is the bound on the number of roots of a polynomial.

This zero estimate is used in Schneider's proof of the Gelfond–Schneider theorem for real numbers: an auxiliary function ∑ᵢⱼ aᵢⱼ zⁱ exp(j z log α) cannot vanish at more real points than the number of its coefficients.

Over the complex numbers, an exponential sum E(z) = ∑ᵢ cᵢ exp(ρᵢ z) with constant coefficients has derivatives E⁽ᵏ⁾(z) = ∑ᵢ cᵢ ρᵢᵏ exp(ρᵢ z). If the frequencies ρᵢ are pairwise distinct and the coefficients are not all zero, then at every point z₀ one of the first N derivatives is nonzero, N being the number of terms, because the Vandermonde matrix of the ρᵢ is invertible. So E vanishes to order less than N everywhere; in particular E is not identically zero. This bounds the order of the first nonvanishing derivative of Gelfond's auxiliary function ∑ₐ,ᵦ ηₐᵦ exp((a + bβ) λ z) in his proof of the Gelfond–Schneider theorem.

Main results

• Finset.hasDerivAt_sum_eval_mul_exp: the derivative of ∑ₖ pₖ(x) exp(γₖ x) is again an exponential polynomial, ∑ₖ (pₖ' + γₖ pₖ)(x) exp(γₖ x).
• TauCeti.card_lt_of_sum_eval_mul_exp_eq_zero: for a nonempty finite index set, pairwise distinct exponents γₖ and nonzero pₖ, a finite set of zeros of ∑ₖ pₖ(x) exp(γₖ x) has fewer than ∑ₖ (deg pₖ + 1) points.
• TauCeti.finite_setOf_sum_eval_mul_exp_eq_zero: under the same hypotheses, the zero set of such a function is finite.
• Finset.iteratedDeriv_sum_mul_cexp: the iterated derivatives of a complex exponential sum.
• TauCeti.exists_lt_card_iteratedDeriv_sum_mul_cexp_ne_zero: with pairwise distinct frequencies and coefficients not all zero, one of the first N derivatives of ∑ᵢ cᵢ exp(ρᵢ z) is nonzero at every point.
• TauCeti.analyticOrderAt_sum_mul_cexp_lt_card: under the same hypotheses, the order of vanishing of ∑ᵢ cᵢ exp(ρᵢ z) at every point is less than the number N of terms.

References

• J.-H. Evertse, Diophantine Approximation, lecture notes (2019), ch. 4, §4.4, Lemma 4.23.
• M. Karatarakis and F. Wiedijk, A formalization of the Gelfond–Schneider theorem, arXiv:2603.24823 (2026), §3.

theorem Finset.hasDerivAt_sum_eval_mul_exp {ι : Type u_1} (s : Finset ι) (γ : ι → ℝ) (p : ι → Polynomial ℝ) (x : ℝ) : HasDerivAt (fun (x : ℝ) => ∑ i ∈ s, Polynomial.eval x (p i) * Real.exp (γ i * x)) (∑ i ∈ s, Polynomial.eval x (Polynomial.derivative (p i) + Polynomial.C (γ i) * p i) * Real.exp (γ i * x)) x

The derivative of ∑ₖ pₖ(x) exp(γₖ x) is ∑ₖ (pₖ' + γₖ pₖ)(x) exp(γₖ x).

theorem TauCeti.card_lt_of_sum_eval_mul_exp_eq_zero {ι : Type u_1} {s : Finset ι} (hs : s.Nonempty) {γ : ι → ℝ} (hγ : Set.InjOn γ ↑s) {p : ι → Polynomial ℝ} (hp : ∀ i ∈ s, p i ≠ 0) {Z : Finset ℝ} (hZ : ∀ x ∈ Z, ∑ i ∈ s, Polynomial.eval x (p i) * Real.exp (γ i * x) = 0) : Z.card < ∑ i ∈ s, ((p i).natDegree + 1)

Zero estimate for real exponential polynomials (Evertse, Lemma 4.23). Let s be a nonempty finite index set, γ exponents that are pairwise distinct on s, and p nonzero real polynomials. Then every finite set Z of zeros of x ↦ ∑ₖ pₖ(x) exp(γₖ x) has fewer than ∑ₖ (deg pₖ + 1) points.

theorem TauCeti.finite_setOf_sum_eval_mul_exp_eq_zero {ι : Type u_1} {s : Finset ι} (hs : s.Nonempty) {γ : ι → ℝ} (hγ : Set.InjOn γ ↑s) {p : ι → Polynomial ℝ} (hp : ∀ i ∈ s, p i ≠ 0) : {x : ℝ | ∑ i ∈ s, Polynomial.eval x (p i) * Real.exp (γ i * x) = 0}.Finite

The zero set of a real exponential polynomial x ↦ ∑ₖ pₖ(x) exp(γₖ x), with nonzero polynomials pₖ and exponents γₖ pairwise distinct on a nonempty finite index set, is finite.

Complex exponential sums

@[simp]

theorem Finset.iteratedDeriv_sum_mul_cexp {ι : Type u_1} (s : Finset ι) (c ρ : ι → ℂ) (k : ℕ) : (iteratedDeriv k fun (z : ℂ) => ∑ i ∈ s, c i * Complex.exp (ρ i * z)) = fun (z : ℂ) => ∑ i ∈ s, c i * ρ i ^ k * Complex.exp (ρ i * z)

The k-th derivative of the exponential sum ∑ᵢ cᵢ exp(ρᵢ z) is ∑ᵢ cᵢ ρᵢᵏ exp(ρᵢ z).

theorem TauCeti.exists_lt_card_iteratedDeriv_sum_mul_cexp_ne_zero {ι : Type u_1} {s : Finset ι} {ρ : ι → ℂ} (hρ : Set.InjOn ρ ↑s) {c : ι → ℂ} (hc : ∃ i ∈ s, c i ≠ 0) (z₀ : ℂ) : ∃ k < s.card, iteratedDeriv k (fun (z : ℂ) => ∑ i ∈ s, c i * Complex.exp (ρ i * z)) z₀ ≠ 0

Let the frequencies ρ be pairwise distinct on a finite set s of indices, and let the coefficients c be nonzero somewhere on s. Then at every point z₀ one of the first #s derivatives of z ↦ ∑ i ∈ s, c i * exp (ρ i * z) is nonzero.

theorem TauCeti.analyticOrderAt_sum_mul_cexp_lt_card {ι : Type u_1} {s : Finset ι} {ρ : ι → ℂ} (hρ : Set.InjOn ρ ↑s) {c : ι → ℂ} (hc : ∃ i ∈ s, c i ≠ 0) (z₀ : ℂ) : analyticOrderAt (fun (z : ℂ) => ∑ i ∈ s, c i * Complex.exp (ρ i * z)) z₀ < ↑s.card

Let the frequencies ρ be pairwise distinct on a finite set s of indices, and let the coefficients c be nonzero somewhere on s. Then the exponential sum z ↦ ∑ i ∈ s, c i * exp (ρ i * z) vanishes to order less than #s at every point. In particular it is not identically zero.