Chebyshev polynomials over the reals: orthogonality

Chebyshev T polynomials are orthogonal with respect to √(1 - x ^ 2)⁻¹.

Main statements

• integrable_measureT: continuous functions are integrable with respect to Lebesgue measure scaled by √(1 - x ^ 2)⁻¹ and restricted to (-1, 1].
• integral_eval_T_real_mul_evalT_real_measureT_of_ne: if n ≠ m then the integral of T_n * T_m equals 0.
• integral_eval_T_real_mul_self_measureT_zero: if n = m = 0 then the integral equals π.
• integral_eval_T_real_mul_self_measureT_of_ne_zero: if n = m ≠ 0 then the integral equals π / 2.

TODO

• Prove that Chebyshev U polynomials are orthogonal with respect to √(1 - x ^ 2)
• Bundle Chebyshev T polynomials into a HilbertBasis for MeasureTheory.Lp ℝ 2 measureT

noncomputable def Polynomial.Chebyshev.measureT : MeasureTheory.Measure ℝ

Lebesgue measure scaled by √(1 - x ^ 2)⁻¹.

Equations

• Polynomial.Chebyshev.measureT = (MeasureTheory.volume.withDensity fun (x : ℝ) => ↑⟨√(1 - x ^ 2)⁻¹, ⋯⟩).restrict (Set.Ioc (-1) 1)

theorem Polynomial.Chebyshev.integral_measureT (f : ℝ → ℝ) : ∫ (x : ℝ), f x ∂measureT = ∫ (x : ℝ) in -1..1, f x * √(1 - x ^ 2)⁻¹

theorem Polynomial.Chebyshev.intervalIntegrable_sqrt_one_sub_sq_inv : IntervalIntegrable (fun (x : ℝ) => √(1 - x ^ 2)⁻¹) MeasureTheory.volume (-1) 1

theorem Polynomial.Chebyshev.integrable_measureT {f : ℝ → ℝ} (hf : ContinuousOn f (Set.Icc (-1) 1)) : MeasureTheory.Integrable f measureT

theorem Polynomial.Chebyshev.integral_measureT_eq_integral_cos {f : ℝ → ℝ} : ∫ (x : ℝ), f x ∂measureT = ∫ (θ : ℝ) in 0..Real.pi, f (Real.cos θ)

@[deprecated Polynomial.Chebyshev.integral_measureT_eq_integral_cos (since := "2026-03-19")]

theorem Polynomial.Chebyshev.integral_measureT_eq_integral_cos_of_continuous {f : ℝ → ℝ} : ∫ (x : ℝ), f x ∂measureT = ∫ (θ : ℝ) in 0..Real.pi, f (Real.cos θ)

Alias of Polynomial.Chebyshev.integral_measureT_eq_integral_cos.

theorem Polynomial.Chebyshev.integral_eval_T_real_measureT_zero : ∫ (x : ℝ), eval x (T ℝ 0) ∂measureT = Real.pi

theorem Polynomial.Chebyshev.integral_eval_T_real_measureT_of_ne_zero {n : ℤ} (hn : n ≠ 0) : ∫ (x : ℝ), eval x (T ℝ n) ∂measureT = 0

theorem Polynomial.Chebyshev.integral_eval_T_real_mul_eval_T_real_measureT (n m : ℤ) : ∫ (x : ℝ), eval x (T ℝ n) * eval x (T ℝ m) ∂measureT = (∫ (x : ℝ), eval x (T ℝ (n + m)) ∂measureT + ∫ (x : ℝ), eval x (T ℝ (n - m)) ∂measureT) / 2

theorem Polynomial.Chebyshev.integral_eval_T_real_mul_eval_T_real_measureT_of_ne {n m : ℕ} (h : n ≠ m) : ∫ (x : ℝ), eval x (T ℝ ↑n) * eval x (T ℝ ↑m) ∂measureT = 0

theorem Polynomial.Chebyshev.integral_eval_T_real_mul_self_measureT_zero : ∫ (x : ℝ), eval x (T ℝ 0) * eval x (T ℝ 0) ∂measureT = Real.pi

theorem Polynomial.Chebyshev.integral_T_real_mul_self_measureT_of_ne_zero {n : ℕ} (hn : n ≠ 0) : ∫ (x : ℝ), eval x (T ℝ ↑n) * eval x (T ℝ ↑n) ∂measureT = Real.pi / 2