Chebyshev polynomials over the reals: Chebyshev–Gauss

The Chebyshev–Gauss property calculates an integral of a polynomial of degree < 2 * n with respect to the weight function √(1 - x ^ 2)⁻¹ supported on [-1, 1] by a sum over appropriate evaluations of the polynomial.

Main statements

• integral_eq_sumZeroes: The integral of a polynomial of degree < 2 * n with respect to the weight function √(1 - x ^ 2)⁻¹ supported on [-1, 1] is equal to π times the average of its values on the points cos ((2 * i + 1) / (2 * n) * π) for 0 ≤ i < n.

Implementation

The statement is proved for Chebyshev polynomials using the complex exponential representation of cos, and then deduced for arbitrary polynomials.

noncomputable def Polynomial.Chebyshev.sumZeroes (n : ℕ) (P : Polynomial ℝ) : ℝ

Weighted sum of P (x) where x goes over cos ((2 * i + 1) / (2 * n) * π) for 0 ≤ i < n.

Equations

• Polynomial.Chebyshev.sumZeroes n P = Real.pi / ↑n * ∑ i ∈ Finset.range n, Polynomial.eval (Real.cos ((2 * ↑i + 1) / (2 * ↑n) * Real.pi)) P

@[simp]

theorem Polynomial.Chebyshev.sumZeroes_sum (n : ℕ) {ι : Type u_1} (s : Finset ι) (P : ι → Polynomial ℝ) : sumZeroes n (∑ i ∈ s, P i) = ∑ i ∈ s, sumZeroes n (P i)

@[simp]

theorem Polynomial.Chebyshev.sumZeroes_smul (n : ℕ) (c : ℝ) (P : Polynomial ℝ) : sumZeroes n (c • P) = c * sumZeroes n P

theorem Polynomial.Chebyshev.sumZeroes_T_zero {n : ℕ} (hn : n ≠ 0) : sumZeroes n (T ℝ 0) = Real.pi

theorem Polynomial.Chebyshev.sumZeroes_T_of_not_dvd {n : ℕ} {k : ℤ} (hk : ¬2 * ↑n ∣ k) : sumZeroes n (T ℝ k) = 0

theorem Polynomial.Chebyshev.integral_eq_sumZeroes {n : ℕ} {P : Polynomial ℝ} (hn : n ≠ 0) (hP : P.degree < 2 * ↑n) : ∫ (x : ℝ), eval x P ∂measureT = sumZeroes n P

The integral of a polynomial of degree < 2 * n with respect to the weight function √(1 - x ^ 2)⁻¹ supported on [-1, 1] is equal to π times the average of its values on the points cos ((2 * i + 1) / (2 * n) * π) for 0 ≤ i < n.