The two Chebyshev normalizations are images of one another

The OrthogonalL2Bases roadmap ships each orthogonal family in two normalizations: the bare polynomials as a basis of the weighted measure, and their √w-envelopes as a basis of the reference measure. For Chebyshev these are TauCeti.chebyshevTHilbertBasis on Polynomial.Chebyshev.measureT and TauCeti.chebyshevTEnvelopeHilbertBasis on volume.restrict (Set.Ioc (-1) 1). Both were assembled separately from the same bridge; nothing so far said they are the same basis seen through the weight-change isometry.

This file says it. The Gaussian instance of the same statement (TauCeti.weightL2Isometry_gaussianHermiteHilbertBasis) has to carry the dilation u = x√2, because the Hermite functions are built on a rescaled argument; the Chebyshev Tₙ are not, so here the identification is exact and can be stated at the level of bases rather than of individual vectors.

The one thing standing in the way was that Polynomial.Chebyshev.measureT is not reducible outside the module defining it, so the identity measureT = w · (volume|_{(-1,1]}) was not available and TauCeti.weightL2Isometry could not be pointed at it. That identity is TauCeti.chebyshevMeasureT_eq_withDensity, recorded with the rest of the Chebyshev measure API in TauCeti.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Measure.

Main statements

• TauCeti.chebyshevWeightL2Isometry — the resulting isometry L²(measureT) ≃ₗᵢ[𝕜] L²((-1, 1]; dx), multiplication by √w.
• TauCeti.chebyshevWeightL2Isometry_normalizedChebyshevTLp — it carries the normalized mode Tₙ/√cₙ to the envelope function τₙ, with no dilation and no change of normalization.
• TauCeti.chebyshevTHilbertBasis_mapₗᵢ and TauCeti.chebyshevTEnvelopeHilbertBasis_mapₗᵢ_symm — the two named Chebyshev Hilbert bases are HilbertBasis.mapₗᵢ-images of one another under that isometry.
• TauCeti.repr_chebyshevWeightL2Isometry — hence a function and its √w-envelope have the same Chebyshev coefficients, so a Chebyshev expansion may be computed in whichever normalization is convenient.

The weight-change isometry for the Chebyshev interval

noncomputable def TauCeti.chebyshevWeightL2Isometry (𝕜 : Type u_1) [RCLike 𝕜] : ↥(MeasureTheory.Lp 𝕜 2 Polynomial.Chebyshev.measureT) ≃ₗᵢ[𝕜] ↥(MeasureTheory.Lp 𝕜 2 (MeasureTheory.volume.restrict (Set.Ioc (-1) 1)))

The Chebyshev weight-change isometry L²(measureT) ≃ₗᵢ[𝕜] L²((-1, 1]; dx): multiplication by √w = (1-x²)^{-1/4}.

This is TauCeti.weightL2Isometry at μ = volume.restrict (Set.Ioc (-1) 1) and w x = (1-x²)^{-1/2}, precomposed with the transport of L²(measureT) along TauCeti.chebyshevMeasureT_eq_withDensity. It is an equivalence, rather than merely an isometric embedding, because the weight is almost everywhere positive on (-1, 1].

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.chebyshevWeightL2Isometry_apply (𝕜 : Type u_1) [RCLike 𝕜] (f : ↥(MeasureTheory.Lp 𝕜 2 Polynomial.Chebyshev.measureT)) : ↑↑((chebyshevWeightL2Isometry 𝕜) f) =ᵐ[MeasureTheory.volume.restrict (Set.Ioc (-1) 1)] fun (x : ℝ) => √√(1 - x ^ 2)⁻¹ • ↑↑f x

The forward isometry multiplies a representative by √w = (1-x²)^{-1/4}. Without this pin the definition would only assert that the two L² spaces are abstractly isometric.

theorem TauCeti.chebyshevWeightL2Isometry_symm_apply (𝕜 : Type u_1) [RCLike 𝕜] (g : ↥(MeasureTheory.Lp 𝕜 2 (MeasureTheory.volume.restrict (Set.Ioc (-1) 1)))) : ↑↑((chebyshevWeightL2Isometry 𝕜).symm g) =ᵐ[MeasureTheory.volume.restrict (Set.Ioc (-1) 1)] fun (x : ℝ) => (√√(1 - x ^ 2)⁻¹)⁻¹ • ↑↑g x

The inverse isometry divides a representative by √w.

The two bases

@[simp]

theorem TauCeti.chebyshevWeightL2Isometry_normalizedChebyshevTLp (𝕜 : Type u_1) [RCLike 𝕜] (n : ℕ) : (chebyshevWeightL2Isometry 𝕜) (normalizedChebyshevTLp 𝕜 n) = chebyshevTEnvelopeLp 𝕜 n

The isometry carries the normalized Chebyshev mode to the envelope function. √w · (Tₙ/√cₙ) = τₙ: the weight moves from the measure into the function, and nothing else changes — no dilation of the argument and no change of normalizing constant.

@[simp]

theorem TauCeti.chebyshevTHilbertBasis_mapₗᵢ (𝕜 : Type u_1) [RCLike 𝕜] : (chebyshevTHilbertBasis 𝕜).mapₗᵢ (chebyshevWeightL2Isometry 𝕜) = chebyshevTEnvelopeHilbertBasis 𝕜

The two Chebyshev bases are the same basis in two normalizations. Transporting the bare-polynomial basis of L²(measureT) across the weight-change isometry gives exactly the envelope basis of L²((-1, 1]; dx).

This is the Chebyshev instance of the roadmap's claim that a family's weighted-measure and √w-envelope bases are HilbertBasis.mapₗᵢ-images of one another; unlike the Gaussian instance it needs no dilation, so it is an equality of bases rather than of individual vectors up to a change of variables.

@[simp]

theorem TauCeti.chebyshevTEnvelopeHilbertBasis_mapₗᵢ_symm (𝕜 : Type u_1) [RCLike 𝕜] : (chebyshevTEnvelopeHilbertBasis 𝕜).mapₗᵢ (chebyshevWeightL2Isometry 𝕜).symm = chebyshevTHilbertBasis 𝕜

The reverse transport: dividing the envelope basis by √w returns the bare-polynomial basis of L²(measureT).

Consequences for coefficients

theorem TauCeti.repr_chebyshevWeightL2Isometry (𝕜 : Type u_1) [RCLike 𝕜] (f : ↥(MeasureTheory.Lp 𝕜 2 Polynomial.Chebyshev.measureT)) : (chebyshevTEnvelopeHilbertBasis 𝕜).repr ((chebyshevWeightL2Isometry 𝕜) f) = (chebyshevTHilbertBasis 𝕜).repr f

A function and its √w-envelope have the same Chebyshev coefficients. The coordinates of √w · f in the envelope basis of L²((-1, 1]; dx) are the coordinates of f in the bare-polynomial basis of L²(measureT), so a Chebyshev expansion may be computed in whichever normalization is convenient.

theorem TauCeti.inner_chebyshevTEnvelopeLp_chebyshevWeightL2Isometry (𝕜 : Type u_1) [RCLike 𝕜] (n : ℕ) (f : ↥(MeasureTheory.Lp 𝕜 2 Polynomial.Chebyshev.measureT)) : inner 𝕜 (chebyshevTEnvelopeLp 𝕜 n) ((chebyshevWeightL2Isometry 𝕜) f) = inner 𝕜 (normalizedChebyshevTLp 𝕜 n) f

The individual coefficient form of TauCeti.repr_chebyshevWeightL2Isometry: pairing the envelope function τₙ against √w · f in L²(dx) is pairing the normalized mode Tₙ/√cₙ against f in L²(measureT).