Parseval and expansions for the Chebyshev cosine Hilbert basis

TauCeti.chebyshevCosineHilbertBasis exhibits the normalized cosines cos (nθ) / √cₙ (where c₀ = π and cₙ = π / 2 for n ≠ 0) as a Hilbert basis of L²((0, π]; dθ) on the angular interval TauCeti.chebyshevAngleMeasure, obtained by transporting TauCeti.chebyshevTHilbertBasis along the cosine isometry TauCeti.chebyshevCosineL2Equiv.

This file supplies the coefficient, Parseval, and Fourier cosine series reconstruction API for that basis. It identifies the abstract coordinates HilbertBasis.repr with both the measure and interval integrals against the normalized cosines, proves Parseval in polarized and norm-square forms, and gives the explicit integral consequence of coordinate transfer across the Chebyshev-to-cosine equivalence.

Main declarations

• TauCeti.chebyshevCosineHilbertBasis_repr_apply — identifies coordinates with measure integrals.
• TauCeti.chebyshevCosineHilbertBasis_repr_apply_interval — identifies coordinates with interval integrals ∫ θ in (0)..π, ….
• TauCeti.tsum_norm_sq_integral_normalizedChebyshevCosine_mul — Parseval's identity in norm-square form.
• TauCeti.tsum_star_integral_normalizedChebyshevCosine_mul_mul_integral — Parseval's identity in polarized form.
• TauCeti.hasSum_chebyshevCosine_expansion — reconstruction of every L² function from its Fourier cosine series.
• TauCeti.integral_normalizedChebyshevCosine_mul_chebyshevCosineL2Equiv — identifies the explicit cosine and Chebyshev integral coefficients across the cosine equivalence.

All statements hold for an arbitrary RCLike scalar field 𝕜, simultaneously covering real- and complex-valued functions.

Coordinate representation

@[simp]

theorem TauCeti.chebyshevCosineHilbertBasis_repr_apply {𝕜 : Type u_1} [RCLike 𝕜] (f : ↥(MeasureTheory.Lp 𝕜 2 chebyshevAngleMeasure)) (n : ℕ) : ↑((chebyshevCosineHilbertBasis 𝕜).repr f) n = ∫ (θ : ℝ), (algebraMap ℝ 𝕜) (normalizedChebyshevCosine n θ) * ↑↑f θ ∂chebyshevAngleMeasure

The n-th coordinate of f in the Chebyshev cosine Hilbert basis is the integral of f against the normalized cosine mode with respect to chebyshevAngleMeasure.

theorem TauCeti.chebyshevCosineHilbertBasis_repr_apply_interval {𝕜 : Type u_1} [RCLike 𝕜] (f : ↥(MeasureTheory.Lp 𝕜 2 chebyshevAngleMeasure)) (n : ℕ) : ↑((chebyshevCosineHilbertBasis 𝕜).repr f) n = ∫ (θ : ℝ) in 0..Real.pi, (algebraMap ℝ 𝕜) (normalizedChebyshevCosine n θ) * ↑↑f θ

The n-th coordinate of f in the Chebyshev cosine Hilbert basis as an interval integral over (0, π].

Parseval identities

theorem TauCeti.tsum_norm_sq_integral_normalizedChebyshevCosine_mul {𝕜 : Type u_1} [RCLike 𝕜] (f : ↥(MeasureTheory.Lp 𝕜 2 chebyshevAngleMeasure)) : ∑' (n : ℕ), ‖∫ (θ : ℝ), (algebraMap ℝ 𝕜) (normalizedChebyshevCosine n θ) * ↑↑f θ ∂chebyshevAngleMeasure‖ ^ 2 = ‖f‖ ^ 2

Parseval's identity for the Chebyshev cosine basis (norm-square form): the squared norms of the explicit cosine integral coefficients of f sum to ‖f‖².

theorem TauCeti.tsum_norm_sq_intervalIntegral_normalizedChebyshevCosine_mul {𝕜 : Type u_1} [RCLike 𝕜] (f : ↥(MeasureTheory.Lp 𝕜 2 chebyshevAngleMeasure)) : ∑' (n : ℕ), ‖∫ (θ : ℝ) in 0..Real.pi, (algebraMap ℝ 𝕜) (normalizedChebyshevCosine n θ) * ↑↑f θ‖ ^ 2 = ‖f‖ ^ 2

Parseval's identity for the Chebyshev cosine basis (interval-integral form): the squared norms of the interval-integral cosine coefficients of f sum to ‖f‖².

theorem TauCeti.tsum_star_integral_normalizedChebyshevCosine_mul_mul_integral {𝕜 : Type u_1} [RCLike 𝕜] (f g : ↥(MeasureTheory.Lp 𝕜 2 chebyshevAngleMeasure)) : ∑' (n : ℕ), star (∫ (θ : ℝ), (algebraMap ℝ 𝕜) (normalizedChebyshevCosine n θ) * ↑↑f θ ∂chebyshevAngleMeasure) * ∫ (θ : ℝ), (algebraMap ℝ 𝕜) (normalizedChebyshevCosine n θ) * ↑↑g θ ∂chebyshevAngleMeasure = inner 𝕜 f g

Parseval's identity for the Chebyshev cosine basis (polarized form): the inner product of f and g is the sum of the conjugated measure-integral coefficients of f times the measure-integral coefficients of g.

theorem TauCeti.tsum_star_intervalIntegral_normalizedChebyshevCosine_mul_mul_intervalIntegral {𝕜 : Type u_1} [RCLike 𝕜] (f g : ↥(MeasureTheory.Lp 𝕜 2 chebyshevAngleMeasure)) : ∑' (n : ℕ), star (∫ (θ : ℝ) in 0..Real.pi, (algebraMap ℝ 𝕜) (normalizedChebyshevCosine n θ) * ↑↑f θ) * ∫ (θ : ℝ) in 0..Real.pi, (algebraMap ℝ 𝕜) (normalizedChebyshevCosine n θ) * ↑↑g θ = inner 𝕜 f g

Parseval's identity for the Chebyshev cosine basis (polarized interval-integral form): the inner product of f and g is the sum of the conjugated interval-integral coefficients of f times the interval-integral coefficients of g.

theorem TauCeti.summable_norm_sq_integral_normalizedChebyshevCosine_mul {𝕜 : Type u_1} [RCLike 𝕜] (f : ↥(MeasureTheory.Lp 𝕜 2 chebyshevAngleMeasure)) : Summable fun (n : ℕ) => ‖∫ (θ : ℝ), (algebraMap ℝ 𝕜) (normalizedChebyshevCosine n θ) * ↑↑f θ ∂chebyshevAngleMeasure‖ ^ 2

The squared norms of the cosine integral coefficients of an L² function are summable.

theorem TauCeti.summable_norm_sq_intervalIntegral_normalizedChebyshevCosine_mul {𝕜 : Type u_1} [RCLike 𝕜] (f : ↥(MeasureTheory.Lp 𝕜 2 chebyshevAngleMeasure)) : Summable fun (n : ℕ) => ‖∫ (θ : ℝ) in 0..Real.pi, (algebraMap ℝ 𝕜) (normalizedChebyshevCosine n θ) * ↑↑f θ‖ ^ 2

The squared norms of the interval-integral cosine coefficients of an L² function are summable.

Series expansion

theorem TauCeti.hasSum_chebyshevCosine_expansion {𝕜 : Type u_1} [RCLike 𝕜] (f : ↥(MeasureTheory.Lp 𝕜 2 chebyshevAngleMeasure)) : HasSum (fun (n : ℕ) => (∫ (θ : ℝ), (algebraMap ℝ 𝕜) (normalizedChebyshevCosine n θ) * ↑↑f θ ∂chebyshevAngleMeasure) • (chebyshevCosineHilbertBasis 𝕜) n) f

The Fourier cosine expansion. Every f ∈ L²((0, π]; dθ) is the sum of its normalized cosine series with respect to chebyshevAngleMeasure.

theorem TauCeti.hasSum_intervalIntegral_chebyshevCosine_expansion {𝕜 : Type u_1} [RCLike 𝕜] (f : ↥(MeasureTheory.Lp 𝕜 2 chebyshevAngleMeasure)) : HasSum (fun (n : ℕ) => (∫ (θ : ℝ) in 0..Real.pi, (algebraMap ℝ 𝕜) (normalizedChebyshevCosine n θ) * ↑↑f θ) • (chebyshevCosineHilbertBasis 𝕜) n) f

The Fourier cosine expansion (interval-integral form). Every f ∈ L²((0, π]; dθ) is the sum of its normalized cosine series with explicit interval integrals over (0, π].

Explicit transfer consequence

theorem TauCeti.integral_normalizedChebyshevCosine_mul_chebyshevCosineL2Equiv {𝕜 : Type u_1} [RCLike 𝕜] (n : ℕ) (g : ↥(MeasureTheory.Lp 𝕜 2 Polynomial.Chebyshev.measureT)) : ∫ (θ : ℝ) in 0..Real.pi, (algebraMap ℝ 𝕜) (normalizedChebyshevCosine n θ) * ↑↑((chebyshevCosineL2Equiv 𝕜) g) θ = ∫ (x : ℝ), (algebraMap ℝ 𝕜) (normalizedChebyshevT n x) * ↑↑g x ∂Polynomial.Chebyshev.measureT

Integral form of coordinate preservation. The angular cosine integral of f ∘ cos over (0, π] equals the Chebyshev-weighted integral of f against Tₙ / √cₙ.