The Chebyshev T polynomials as a Hilbert basis of L²(measureT)

Roadmap Part C: the normalized Chebyshev T modes Tₙ/√‖Tₙ‖² are a Hilbert basis of L²([-1,1]; measureT), where measureT is Mathlib's Chebyshev orthogonality measure (weight (1-x²)^{-1/2}).

Every input is already merged; this file only supplies the missing assembly. Orthonormality is TauCeti.orthonormal_normalizedChebyshevTLp; completeness is the one step that had been left open, because it needs the function-level moment-determinacy theorem TauCeti.ae_eq_zero_of_forall_moment_eq_zero_of_exists_integrable_exp (a vector of L²(measureT) orthogonal to every monomial is a.e. 0). That theorem asks only for a single positive rate a with e^{a|x|} integrable, which is free here: the Chebyshev measure has compact support [-1,1], so e^{|x|} is integrable against it and a = 1 works.

The bridge from mode-orthogonality to monomial-orthogonality is TauCeti.inner_polynomialEvalChebyshevLp_eq_zero.

Main statements

• TauCeti.chebyshevTHilbertBasis — the Chebyshev T Hilbert basis of L²(measureT).
• TauCeti.coe_chebyshevTHilbertBasis — the anti-vacuity pin: the n-th basis vector is the normalized mode Tₙ/√‖Tₙ‖².

theorem TauCeti.monomial_moment_measureT_eq_zero (𝕜 : Type u_1) [RCLike 𝕜] (g : ↥(MeasureTheory.Lp 𝕜 2 Polynomial.Chebyshev.measureT)) (hmode : ∀ (n : ℕ), inner 𝕜 g (normalizedChebyshevTLp 𝕜 n) = 0) (n : ℕ) : ∫ (x : ℝ), (algebraMap ℝ 𝕜) x ^ n * ↑↑g x ∂Polynomial.Chebyshev.measureT = 0

Monomial-orthogonality from mode-orthogonality. A vector of L²(measureT) orthogonal to every normalized Chebyshev mode has every scalar-cast monomial moment ∫ (x : 𝕜)ⁿ · g vanishing. This threads inner_polynomialEvalChebyshevLp_eq_zero (orthogonality to every polynomial evaluation) through the L² inner product at q = Xⁿ.

theorem TauCeti.orthogonal_span_normalizedChebyshevTLp_eq_bot (𝕜 : Type u_1) [RCLike 𝕜] : (Submodule.span 𝕜 (Set.range (normalizedChebyshevTLp 𝕜)))ᗮ = ⊥

Completeness of the Chebyshev family. The orthogonal complement of the span of the normalized modes is trivial: a vector orthogonal to all of them has vanishing monomial moments and is therefore a.e. 0 by moment determinacy.

noncomputable def TauCeti.chebyshevTHilbertBasis (𝕜 : Type u_1) [RCLike 𝕜] : HilbertBasis ℕ 𝕜 ↥(MeasureTheory.Lp 𝕜 2 Polynomial.Chebyshev.measureT)

Roadmap Part C: the Chebyshev T polynomials are a Hilbert basis of L²(measureT). Orthonormality is orthonormal_normalizedChebyshevTLp; completeness is orthogonal_span_normalizedChebyshevTLp_eq_bot, which is where the shipped Chebyshev groundwork had stopped, one step short of the function-level moment-determinacy theorem.

Equations

• TauCeti.chebyshevTHilbertBasis 𝕜 = HilbertBasis.mkOfOrthogonalEqBot ⋯ ⋯

@[simp]

theorem TauCeti.coe_chebyshevTHilbertBasis (𝕜 : Type u_1) [RCLike 𝕜] : ⇑(chebyshevTHilbertBasis 𝕜) = normalizedChebyshevTLp 𝕜

The basis vectors are the normalized Chebyshev modes. Without this the construction would only exhibit some Hilbert basis of L²(measureT); here each vector is pinned to Tₙ/√‖Tₙ‖².