Polynomial span of the Chebyshev modes

This file connects the algebraic Chebyshev basis of ℝ[X] with the normalized Chebyshev functions in L²(Polynomial.Chebyshev.measureT). Evaluation followed by the canonical map into L² is bundled as a linear map. Since every Chebyshev polynomial is a nonzero scalar multiple of its normalized mode, every polynomial evaluation belongs to the linear span of those modes.

This is the algebra-to-analysis handoff in Part C of the OrthogonalL2Bases roadmap. In the completeness argument, it upgrades orthogonality against every Chebyshev mode to orthogonality against every polynomial.

Main declarations

• TauCeti.polynomialEvalChebyshevLp: polynomial evaluation, cast into any [RCLike 𝕜] scalar field, as a linear map into L²(Polynomial.Chebyshev.measureT).
• TauCeti.polynomialEvalChebyshevLp_mem_span: every polynomial evaluation lies in the span of the normalized Chebyshev modes.
• TauCeti.inner_polynomialEvalChebyshevLp_eq_zero: orthogonality to all normalized modes implies orthogonality to every polynomial evaluation.
• TauCeti.inner_polynomialEvalChebyshevLp: the inner product against a polynomial evaluation is the corresponding polynomial moment ∫ x, g x * q.eval x ∂measureT.
• TauCeti.integral_polynomialEval_measureT_eq_zero: orthogonality to all normalized modes makes every polynomial moment vanish.

The measure- and scalar-generic bundling of polynomial evaluation lives in TauCeti.MeasureTheory.Function.PolynomialMemLp as polynomialEvalLp; polynomialEvalChebyshevLp is its Chebyshev specialization.

theorem TauCeti.polynomialEvalChebyshevLp_T (𝕜 : Type u_1) [RCLike 𝕜] (n : ℕ) : (polynomialEvalChebyshevLp 𝕜) (Polynomial.Chebyshev.T ℝ ↑n) = √(chebyshevTNormSq n) • normalizedChebyshevTLp 𝕜 n

Under the polynomial-evaluation map, the nth Chebyshev polynomial is the square root of its squared norm times the normalized nth Chebyshev mode.

theorem TauCeti.polynomialEvalChebyshevLp_mem_span (𝕜 : Type u_1) [RCLike 𝕜] (q : Polynomial ℝ) : (polynomialEvalChebyshevLp 𝕜) q ∈ Submodule.span 𝕜 (Set.range (normalizedChebyshevTLp 𝕜))

Every real polynomial evaluation in L²(measureT) belongs to the linear span of the normalized Chebyshev modes.

theorem TauCeti.inner_polynomialEvalChebyshevLp_eq_zero (𝕜 : Type u_1) [RCLike 𝕜] (g : ↥(MeasureTheory.Lp 𝕜 2 Polynomial.Chebyshev.measureT)) (hmode : ∀ (n : ℕ), inner 𝕜 g (normalizedChebyshevTLp 𝕜 n) = 0) (q : Polynomial ℝ) : inner 𝕜 g ((polynomialEvalChebyshevLp 𝕜) q) = 0

A vector orthogonal to every normalized Chebyshev mode is orthogonal to the L² evaluation of every real polynomial.

This is the abstract form used in the Chebyshev completeness argument: the algebraic Chebyshev basis converts the mode hypotheses into orthogonality against every polynomial evaluation.

theorem TauCeti.inner_polynomialEvalChebyshevLp (g : ↥(MeasureTheory.Lp ℝ 2 Polynomial.Chebyshev.measureT)) (q : Polynomial ℝ) : inner ℝ g ((polynomialEvalChebyshevLp ℝ) q) = ∫ (x : ℝ), ↑↑g x * Polynomial.eval x q ∂Polynomial.Chebyshev.measureT

The inner product of a vector with a polynomial evaluation is the corresponding polynomial moment against the Chebyshev measure.

theorem TauCeti.integral_polynomialEval_measureT_eq_zero (g : ↥(MeasureTheory.Lp ℝ 2 Polynomial.Chebyshev.measureT)) (hmode : ∀ (n : ℕ), inner ℝ g (normalizedChebyshevTLp ℝ n) = 0) (q : Polynomial ℝ) : ∫ (x : ℝ), ↑↑g x * Polynomial.eval x q ∂Polynomial.Chebyshev.measureT = 0

A vector orthogonal to every normalized Chebyshev mode has vanishing polynomial moments: this is the concrete integral form of inner_polynomialEvalChebyshevLp_eq_zero.