Parseval and expansions for the Chebyshev T basis

TauCeti.chebyshevTHilbertBasis exhibits the normalized Chebyshev polynomials Tₙ / √cₙ, where c₀ = π and cₙ = π / 2 for n ≠ 0, as a Hilbert basis of L²(Polynomial.Chebyshev.measureT). This file supplies the coefficient, Parseval, and reconstruction API for that basis. Its coordinate theorem identifies the abstract HilbertBasis.repr coordinate with the Chebyshev-weighted integral against the normalized polynomial.

The API and proof structure are adapted from TauCeti.Probability.Distributions.Gaussian.Hermite.Parseval.

Main statements

• TauCeti.chebyshevTHilbertBasis_repr_apply identifies each coordinate with its weighted integral.
• TauCeti.tsum_norm_sq_integral_normalizedChebyshevT_mul_measureT is the norm-square Parseval identity for the explicit integral coefficients.
• TauCeti.summable_norm_sq_integral_normalizedChebyshevT_mul_measureT gives their square-summability.
• TauCeti.hasSum_chebyshevT_expansion reconstructs every L² vector from its Chebyshev series.

All statements hold over an arbitrary RCLike scalar field, simultaneously covering real- and complex-valued functions.

@[simp]

theorem TauCeti.chebyshevTHilbertBasis_repr_apply {𝕜 : Type u_1} [RCLike 𝕜] (f : ↥(MeasureTheory.Lp 𝕜 2 Polynomial.Chebyshev.measureT)) (n : ℕ) : ↑((chebyshevTHilbertBasis 𝕜).repr f) n = ∫ (x : ℝ), (algebraMap ℝ 𝕜) (normalizedChebyshevT n x) * ↑↑f x ∂Polynomial.Chebyshev.measureT

The n-th Chebyshev coordinate is the integral of f against the normalized polynomial Tₙ / √cₙ with respect to the Chebyshev measure.

theorem TauCeti.tsum_norm_sq_integral_normalizedChebyshevT_mul_measureT {𝕜 : Type u_1} [RCLike 𝕜] (f : ↥(MeasureTheory.Lp 𝕜 2 Polynomial.Chebyshev.measureT)) : ∑' (n : ℕ), ‖∫ (x : ℝ), (algebraMap ℝ 𝕜) (normalizedChebyshevT n x) * ↑↑f x ∂Polynomial.Chebyshev.measureT‖ ^ 2 = ‖f‖ ^ 2

Parseval's identity for the Chebyshev basis. The squared norms of the explicit Chebyshev integral coefficients of f sum to ‖f‖².

theorem TauCeti.summable_norm_sq_integral_normalizedChebyshevT_mul_measureT {𝕜 : Type u_1} [RCLike 𝕜] (f : ↥(MeasureTheory.Lp 𝕜 2 Polynomial.Chebyshev.measureT)) : Summable fun (n : ℕ) => ‖∫ (x : ℝ), (algebraMap ℝ 𝕜) (normalizedChebyshevT n x) * ↑↑f x ∂Polynomial.Chebyshev.measureT‖ ^ 2

The squared norms of the Chebyshev integral coefficients of an L² function are summable.

theorem TauCeti.hasSum_chebyshevT_expansion {𝕜 : Type u_1} [RCLike 𝕜] (f : ↥(MeasureTheory.Lp 𝕜 2 Polynomial.Chebyshev.measureT)) : HasSum (fun (n : ℕ) => (∫ (x : ℝ), (algebraMap ℝ 𝕜) (normalizedChebyshevT n x) * ↑↑f x ∂Polynomial.Chebyshev.measureT) • normalizedChebyshevTLp 𝕜 n) f

The Chebyshev expansion. Every f ∈ L²(measureT) is the sum of its normalized Chebyshev-polynomial series.