The Chebyshev basis as a cosine basis

Transporting TauCeti.chebyshevTHilbertBasis across TauCeti.chebyshevCosineL2Equiv gives a Hilbert basis on the angular interval. Its nth vector is the normalized cosine cos (nθ) / √cₙ, where c₀ = π and cₙ = π / 2 for n > 0. This is the unitary-transfer statement required by Part C of the OrthogonalL2Bases roadmap.

Main declarations

• TauCeti.chebyshevCosineHilbertBasis is the transported Chebyshev basis.
• TauCeti.coeFn_chebyshevCosineHilbertBasis identifies its vectors with the normalized cosines.
• TauCeti.chebyshevCosineL2Equiv_normalizedChebyshevTLp identifies the transported normalized Chebyshev modes.
• TauCeti.chebyshevCosineHilbertBasis_repr_chebyshevCosineL2Equiv identifies coordinates across the cosine equivalence.

noncomputable def TauCeti.chebyshevCosineHilbertBasis (𝕜 : Type u_1) [RCLike 𝕜] : HilbertBasis ℕ 𝕜 ↥(MeasureTheory.Lp 𝕜 2 chebyshevAngleMeasure)

The normalized cosine Hilbert basis of L²((0, π]), obtained by transporting the normalized Chebyshev T basis under x = cos θ.

Equations

• TauCeti.chebyshevCosineHilbertBasis 𝕜 = (TauCeti.chebyshevTHilbertBasis 𝕜).mapₗᵢ (TauCeti.chebyshevCosineL2Equiv 𝕜)

theorem TauCeti.coeFn_chebyshevCosineHilbertBasis (𝕜 : Type u_1) [RCLike 𝕜] (n : ℕ) : ↑↑((chebyshevCosineHilbertBasis 𝕜) n) =ᵐ[chebyshevAngleMeasure] fun (θ : ℝ) => (algebraMap ℝ 𝕜) (normalizedChebyshevCosine n θ)

Chebyshev-cosine basis correspondence. The nth vector of the transported Chebyshev basis is almost everywhere the scalar-cast normalized cosine cos (nθ) / √cₙ.

Transfer across the cosine change of variables

@[simp]

theorem TauCeti.chebyshevCosineL2Equiv_normalizedChebyshevTLp (𝕜 : Type u_1) [RCLike 𝕜] (n : ℕ) : (chebyshevCosineL2Equiv 𝕜) (normalizedChebyshevTLp 𝕜 n) = (chebyshevCosineHilbertBasis 𝕜) n

The cosine change of variables carries Chebyshev polynomial modes to cosine modes. chebyshevCosineL2Equiv maps the normalized Chebyshev mode Tₙ / √cₙ in L²(measureT) to the normalized angular cosine mode cos (nθ) / √cₙ in L²(chebyshevAngleMeasure).

@[simp]

theorem TauCeti.chebyshevCosineL2Equiv_symm_chebyshevCosineHilbertBasis (𝕜 : Type u_1) [RCLike 𝕜] (n : ℕ) : (chebyshevCosineL2Equiv 𝕜).symm ((chebyshevCosineHilbertBasis 𝕜) n) = normalizedChebyshevTLp 𝕜 n

The inverse cosine equivalence maps the normalized cosine mode back to the normalized Chebyshev polynomial mode.

theorem TauCeti.chebyshevCosineHilbertBasis_repr_chebyshevCosineL2Equiv (𝕜 : Type u_1) [RCLike 𝕜] (g : ↥(MeasureTheory.Lp 𝕜 2 Polynomial.Chebyshev.measureT)) (n : ℕ) : ↑((chebyshevCosineHilbertBasis 𝕜).repr ((chebyshevCosineL2Equiv 𝕜) g)) n = ↑((chebyshevTHilbertBasis 𝕜).repr g) n

Coordinates are preserved under the cosine change of variables. The n-th coordinate of f ∘ cos in the Chebyshev cosine basis equals the n-th coordinate of f in the Chebyshev polynomial basis.

theorem TauCeti.chebyshevTHilbertBasis_repr_chebyshevCosineL2Equiv_symm (𝕜 : Type u_1) [RCLike 𝕜] (f : ↥(MeasureTheory.Lp 𝕜 2 chebyshevAngleMeasure)) (n : ℕ) : ↑((chebyshevTHilbertBasis 𝕜).repr ((chebyshevCosineL2Equiv 𝕜).symm f)) n = ↑((chebyshevCosineHilbertBasis 𝕜).repr f) n

The inverse coordinate identification: the Chebyshev polynomial coordinate of f ∘ arccos equals the cosine coordinate of f.

@[simp]

theorem TauCeti.inner_chebyshevCosineHilbertBasis_chebyshevCosineL2Equiv (𝕜 : Type u_1) [RCLike 𝕜] (n : ℕ) (g : ↥(MeasureTheory.Lp 𝕜 2 Polynomial.Chebyshev.measureT)) : inner 𝕜 ((chebyshevCosineHilbertBasis 𝕜) n) ((chebyshevCosineL2Equiv 𝕜) g) = inner 𝕜 (normalizedChebyshevTLp 𝕜 n) g

Pairing against the normalized cosine mode in L²(chebyshevAngleMeasure) is pairing against the normalized Chebyshev polynomial mode in L²(measureT).