Fourier Coefficients of Polynomials

We define an algebra map from ℂ[X] to the MeasureTheory.Lp (with p := 2) space on the additive circle and show that it sends monomials to the Fourier basis. From this, we derive that polynomial coefficients match Fourier coefficients and prove Parseval's identity for polynomials.

Main definitions

• Polynomial.toAddCircle: Algebra map from ℂ[X] to C(AddCircle (2 * π), ℂ) that evaluates polynomials on the unit circle.

Main results

• Polynomial.fourierCoeff_toAddCircle: The n-th Fourier coefficient of a polynomial equals its n-th coefficient when n is nonnegative, else 0.
• Polynomial.fourierCoeff_toAddCircle_natCast: A variant of Polynomial.fourierCoeff_toAddCircle for ℕ arguments.
• Polynomial.sum_sq_norm_coeff_eq_circleAverage: Parseval's identity that the sum of the squares of the norms of the coefficients of a polynomial equals the average over the circle of the norm square of the polynomial.

theorem Polynomial.instTwoPiPos : Fact (0 < 2 * Real.pi)

noncomputable def Polynomial.toAddCircle : Polynomial ℂ →ₐ[ℂ] C(AddCircle (2 * Real.pi), ℂ)

Algebra map from ℂ[X] to C(AddCircle (2 * π), ℂ) that evaluates polynomials on the unit circle. For a polynomial p, this maps it to the function fun θ ↦ p (exp (I * θ)).

theorem Polynomial.toAddCircle.integrable (p : Polynomial ℂ) : MeasureTheory.Integrable (⇑(toAddCircle p)) AddCircle.haarAddCircle

theorem Polynomial.toAddCircle_C_eq_smul_fourier_zero {c : ℂ} : toAddCircle (C c) = c • fourier 0

theorem Polynomial.toAddCircle_X_eq_fourier_one : toAddCircle X = fourier 1

theorem Polynomial.toAddCircle_X_pow_eq_fourier {n : ℕ} : toAddCircle (X ^ n) = fourier ↑n

theorem Polynomial.toAddCircle_monomial_eq_smul_fourier {n : ℕ} {c : ℂ} : toAddCircle ((monomial n) c) = c • fourier ↑n

theorem Polynomial.fourierCoeff_toAddCircle (p : Polynomial ℂ) (n : ℤ) : fourierCoeff (⇑(toAddCircle p)) n = if 0 ≤ n then p.coeff n.natAbs else 0

The nth Fourier coefficient of a polynomial is the coefficient of X ^ n, or zero if n < 0.

theorem Polynomial.fourierCoeff_toAddCircle_natCast (p : Polynomial ℂ) (n : ℕ) : fourierCoeff ⇑(toAddCircle p) ↑n = p.coeff n

The nth Fourier coefficient of a polynomial is the coefficient of X ^ n

theorem Polynomial.fourierCoeff_toAddCircle_eq_zero_of_lt_zero (p : Polynomial ℂ) (n : ℤ) (hn : n < 0) : fourierCoeff (⇑(toAddCircle p)) n = 0

theorem Polynomial.sum_sq_norm_coeff_eq_circleAverage (p : Polynomial ℂ) : ∑ i ∈ p.support, ‖p.coeff i‖ ^ 2 = Real.circleAverage (fun (θ : ℂ) => ‖eval θ p‖ ^ 2) 0 1

Parseval's Identity for polynomials