Polynomial moments for the Chebyshev T measure

This file records bare-polynomial moment, L¹, and L² consequences of compact support for Mathlib's Chebyshev orthogonality measure Polynomial.Chebyshev.measureT.

The normalized Chebyshev modes and their orthonormality live in TauCeti.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Measure. The lemmas here are the un-normalized consumer forms needed on the way to the roadmap's Chebyshev Hilbert-basis target: every real polynomial moment is finite, every real polynomial evaluation is integrable and square integrable, and these statements are available after casting real-valued functions to any [RCLike 𝕜] scalar field.

theorem TauCeti.integrable_pow_measureT (k : ℕ) : MeasureTheory.Integrable (fun (x : ℝ) => x ^ k) Polynomial.Chebyshev.measureT

Every real monomial has finite L¹ moment with respect to the Chebyshev T measure.

theorem TauCeti.integrable_eval_measureT (q : Polynomial ℝ) : MeasureTheory.Integrable (fun (x : ℝ) => Polynomial.eval x q) Polynomial.Chebyshev.measureT

A real polynomial evaluation is integrable with respect to the Chebyshev T measure.

theorem TauCeti.integrable_algebraMap_eval_measureT {𝕜 : Type u_1} [RCLike 𝕜] (q : Polynomial ℝ) : MeasureTheory.Integrable (fun (x : ℝ) => (algebraMap ℝ 𝕜) (Polynomial.eval x q)) Polynomial.Chebyshev.measureT

A real polynomial evaluation, cast to any RCLike scalar field, is integrable with respect to the Chebyshev T measure.

theorem TauCeti.memLp_two_eval_measureT (q : Polynomial ℝ) : MeasureTheory.MemLp (fun (x : ℝ) => Polynomial.eval x q) 2 Polynomial.Chebyshev.measureT

A real polynomial evaluation lies in L² with respect to the Chebyshev T measure.

theorem TauCeti.memLp_two_algebraMap_eval_measureT {𝕜 : Type u_1} [RCLike 𝕜] (q : Polynomial ℝ) : MeasureTheory.MemLp (fun (x : ℝ) => (algebraMap ℝ 𝕜) (Polynomial.eval x q)) 2 Polynomial.Chebyshev.measureT

A real polynomial evaluation, cast to any RCLike scalar field, lies in L² with respect to the Chebyshev T measure.

noncomputable def TauCeti.polynomialEvalChebyshevLp (𝕜 : Type u_1) [RCLike 𝕜] : Polynomial ℝ →ₗ[ℝ] ↥(MeasureTheory.Lp 𝕜 2 Polynomial.Chebyshev.measureT)

Evaluate a real polynomial and, casting into any [RCLike 𝕜] scalar field, regard the result as an element of L²(Polynomial.Chebyshev.measureT).

The map is well-defined because every polynomial has finite second moment for the Chebyshev measure.

Equations

• TauCeti.polynomialEvalChebyshevLp 𝕜 = TauCeti.polynomialEvalLp 𝕜 TauCeti.integrable_pow_measureT

theorem TauCeti.coeFn_polynomialEvalChebyshevLp (𝕜 : Type u_1) [RCLike 𝕜] (q : Polynomial ℝ) : ↑↑((polynomialEvalChebyshevLp 𝕜) q) =ᵐ[Polynomial.Chebyshev.measureT] fun (x : ℝ) => (algebraMap ℝ 𝕜) (Polynomial.eval x q)

The L² representative of a polynomial evaluation is the expected scalar-cast pointwise evaluation.