Chebyshev T transfer to the cosine side

This file packages the cosine-side consequences of Mathlib's change-of-variables identity Polynomial.Chebyshev.integral_measureT_eq_integral_cos. It provides the one-dimensional integral API, the equivalence between the Chebyshev and angular measures, and the induced L² equivalence under x = cos θ. The roadmap's Chebyshev Hilbert-basis target uses this infrastructure to identify the normalized Chebyshev functions on measureT with the cosine basis.

Main declarations

• TauCeti.chebyshevAngleMeasure is Lebesgue measure restricted to (0, π].
• TauCeti.chebyshevCosineL2Equiv pulls an L²(measureT) function back along Real.cos.
• TauCeti.normalizedChebyshevCosine is the normalized angular cosine mode.

noncomputable def TauCeti.chebyshevAngleMeasure : MeasureTheory.Measure ℝ

Lebesgue measure on the angular interval (0, π]. The choice of half-open endpoints matches intervalIntegral.integral_of_le; changing either endpoint does not change the measure.

Equations

• TauCeti.chebyshevAngleMeasure = MeasureTheory.volume.restrict (Set.Ioc 0 Real.pi)

theorem TauCeti.chebyshevAngleMeasure_def : chebyshevAngleMeasure = MeasureTheory.volume.restrict (Set.Ioc 0 Real.pi)

The angular Chebyshev measure is Lebesgue measure restricted to (0, π].

theorem TauCeti.integral_chebyshevAngleMeasure {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ℝ → E) : ∫ (θ : ℝ), f θ ∂chebyshevAngleMeasure = ∫ (θ : ℝ) in 0..Real.pi, f θ

Integrating against chebyshevAngleMeasure is interval integration from 0 to π.

theorem TauCeti.map_cos_chebyshevAngleMeasure : MeasureTheory.Measure.map Real.cos chebyshevAngleMeasure = Polynomial.Chebyshev.measureT

The pushforward of angular Lebesgue measure under cos is the Chebyshev measure.

theorem TauCeti.measurePreserving_cos_chebyshev : MeasureTheory.MeasurePreserving Real.cos chebyshevAngleMeasure Polynomial.Chebyshev.measureT

The cosine change of variables preserves chebyshevAngleMeasure and measureT.

theorem TauCeti.measurePreserving_arccos_chebyshev : MeasureTheory.MeasurePreserving Real.arccos Polynomial.Chebyshev.measureT chebyshevAngleMeasure

The inverse change of variables arccos preserves the Chebyshev and angular measures.

noncomputable def TauCeti.chebyshevCosineL2Equiv (𝕜 : Type u_1) [NormedRing 𝕜] : ↥(MeasureTheory.Lp 𝕜 2 Polynomial.Chebyshev.measureT) ≃ₗᵢ[𝕜] ↥(MeasureTheory.Lp 𝕜 2 chebyshevAngleMeasure)

The Chebyshev-to-cosine L² equivalence. It pulls a function on [-1,1] back along x = cos θ; its inverse pulls an angular function back along θ = arccos x.

Equations

• TauCeti.chebyshevCosineL2Equiv 𝕜 = MeasureTheory.Lp.compMeasurePreservingₗᵢEquiv 𝕜 TauCeti.measurePreserving_cos_chebyshev TauCeti.measurePreserving_arccos_chebyshev TauCeti.cos_comp_arccos_ae✝

theorem TauCeti.chebyshevCosineL2Equiv_apply (𝕜 : Type u_1) [NormedRing 𝕜] (f : ↥(MeasureTheory.Lp 𝕜 2 Polynomial.Chebyshev.measureT)) : ↑↑((chebyshevCosineL2Equiv 𝕜) f) =ᵐ[chebyshevAngleMeasure] fun (θ : ℝ) => ↑↑f (Real.cos θ)

The forward Chebyshev-to-cosine equivalence is composition with Real.cos.

theorem TauCeti.chebyshevCosineL2Equiv_symm_apply (𝕜 : Type u_1) [NormedRing 𝕜] (f : ↥(MeasureTheory.Lp 𝕜 2 chebyshevAngleMeasure)) : ↑↑((chebyshevCosineL2Equiv 𝕜).symm f) =ᵐ[Polynomial.Chebyshev.measureT] fun (x : ℝ) => ↑↑f (Real.arccos x)

The inverse Chebyshev-to-cosine equivalence is composition with Real.arccos.

noncomputable def TauCeti.chebyshevCosine (n : ℕ) (θ : ℝ) : ℝ

The cosine-side representative corresponding to the Chebyshev polynomial Tₙ.

Equations

• TauCeti.chebyshevCosine n θ = Real.cos (↑n * θ)

theorem TauCeti.chebyshevCosine_def (n : ℕ) (θ : ℝ) : chebyshevCosine n θ = Real.cos (↑n * θ)

The defining equation for the cosine-side Chebyshev representative.

@[simp]

theorem TauCeti.chebyshevCosine_zero (θ : ℝ) : chebyshevCosine 0 θ = 1

@[simp]

theorem TauCeti.chebyshevCosine_one (θ : ℝ) : chebyshevCosine 1 θ = Real.cos θ

theorem TauCeti.eval_T_real_cos_eq_chebyshevCosine (n : ℕ) (θ : ℝ) : Polynomial.eval (Real.cos θ) (Polynomial.Chebyshev.T ℝ ↑n) = chebyshevCosine n θ

Chebyshev polynomials restrict along x = cos θ to the cosine functions.

theorem TauCeti.continuous_chebyshevCosine (n : ℕ) : Continuous (chebyshevCosine n)

The cosine-side representatives are continuous.

theorem TauCeti.integral_eval_T_real_measureT_eq_integral_chebyshevCosine (n : ℕ) : ∫ (x : ℝ), Polynomial.eval x (Polynomial.Chebyshev.T ℝ ↑n) ∂Polynomial.Chebyshev.measureT = ∫ (θ : ℝ) in 0..Real.pi, chebyshevCosine n θ

Transfer a single Chebyshev T integral from measureT to the angular cosine-side integral.

theorem TauCeti.integral_eval_T_real_mul_eval_T_real_measureT_eq_integral_chebyshevCosine_mul (m n : ℕ) : ∫ (x : ℝ), Polynomial.eval x (Polynomial.Chebyshev.T ℝ ↑m) * Polynomial.eval x (Polynomial.Chebyshev.T ℝ ↑n) ∂Polynomial.Chebyshev.measureT = ∫ (θ : ℝ) in 0..Real.pi, chebyshevCosine m θ * chebyshevCosine n θ

Transfer a product of two Chebyshev T polynomials from measureT to the angular cosine-side integral.

theorem TauCeti.integral_chebyshevCosine_zero : ∫ (θ : ℝ) in 0..Real.pi, chebyshevCosine 0 θ = Real.pi

The cosine-side integral of the constant Chebyshev mode.

theorem TauCeti.integral_chebyshevCosine_of_ne_zero {n : ℕ} (hn : n ≠ 0) : ∫ (θ : ℝ) in 0..Real.pi, chebyshevCosine n θ = 0

Nonzero cosine modes have zero integral over [0, π].

theorem TauCeti.integral_chebyshevCosine_mul_self (n : ℕ) : ∫ (θ : ℝ) in 0..Real.pi, chebyshevCosine n θ * chebyshevCosine n θ = chebyshevTNormSq n

The diagonal cosine-side L² integral, using the same squared-norm constant as the Chebyshev T polynomials.

theorem TauCeti.integral_chebyshevCosine_mul_chebyshevCosine_of_ne {m n : ℕ} (hmn : m ≠ n) : ∫ (θ : ℝ) in 0..Real.pi, chebyshevCosine m θ * chebyshevCosine n θ = 0

Off-diagonal cosine modes are orthogonal over [0, π].

theorem TauCeti.integral_chebyshevCosine_mul_chebyshevCosine_eq_ite (m n : ℕ) : ∫ (θ : ℝ) in 0..Real.pi, chebyshevCosine m θ * chebyshevCosine n θ = if m = n then chebyshevTNormSq n else 0

Cosine-side Chebyshev orthogonality in the Kronecker-delta form expected by the later Chebyshev Hilbert-basis construction.

Normalized cosine modes

noncomputable def TauCeti.normalizedChebyshevCosine (n : ℕ) (θ : ℝ) : ℝ

The normalized angular cosine mode corresponding to the normalized Chebyshev Tₙ mode.

Equations

• TauCeti.normalizedChebyshevCosine n θ = TauCeti.chebyshevCosine n θ / √(TauCeti.chebyshevTNormSq n)

theorem TauCeti.normalizedChebyshevCosine_def (n : ℕ) (θ : ℝ) : normalizedChebyshevCosine n θ = chebyshevCosine n θ / √(chebyshevTNormSq n)

The defining equation for the normalized angular cosine representative.

@[simp]

theorem TauCeti.normalizedChebyshevCosine_zero (θ : ℝ) : normalizedChebyshevCosine 0 θ = 1 / √Real.pi

@[simp]

theorem TauCeti.normalizedChebyshevCosine_one (θ : ℝ) : normalizedChebyshevCosine 1 θ = Real.cos θ / √(Real.pi / 2)

@[simp]

theorem TauCeti.normalizedChebyshevCosine_of_ne_zero {n : ℕ} (hn : n ≠ 0) (θ : ℝ) : normalizedChebyshevCosine n θ = Real.cos (↑n * θ) / √(Real.pi / 2)

theorem TauCeti.continuous_normalizedChebyshevCosine (n : ℕ) : Continuous (normalizedChebyshevCosine n)

The normalized angular Chebyshev representatives are continuous.

theorem TauCeti.normalized_eval_T_real_cos_eq_normalizedChebyshevCosine (n : ℕ) (θ : ℝ) : Polynomial.eval (Real.cos θ) (Polynomial.Chebyshev.T ℝ ↑n) / √(chebyshevTNormSq n) = normalizedChebyshevCosine n θ

Pulling back a normalized Chebyshev T polynomial along x = cos θ gives the normalized angular cosine mode.

theorem TauCeti.integral_normalized_eval_T_real_mul_measureT_eq_integral_normalizedChebyshevCosine_mul (m n : ℕ) : ∫ (x : ℝ), Polynomial.eval x (Polynomial.Chebyshev.T ℝ ↑m) / √(chebyshevTNormSq m) * (Polynomial.eval x (Polynomial.Chebyshev.T ℝ ↑n) / √(chebyshevTNormSq n)) ∂Polynomial.Chebyshev.measureT = ∫ (θ : ℝ) in 0..Real.pi, normalizedChebyshevCosine m θ * normalizedChebyshevCosine n θ

Transfer a product of normalized Chebyshev T polynomials from measureT to the normalized angular cosine-side integral.

theorem TauCeti.integral_normalizedChebyshevCosine_mul_self (n : ℕ) : ∫ (θ : ℝ) in 0..Real.pi, normalizedChebyshevCosine n θ * normalizedChebyshevCosine n θ = 1

The diagonal normalized angular cosine modes have integral one over [0, π].

theorem TauCeti.integral_normalizedChebyshevCosine_mul_normalizedChebyshevCosine_of_ne {m n : ℕ} (hmn : m ≠ n) : ∫ (θ : ℝ) in 0..Real.pi, normalizedChebyshevCosine m θ * normalizedChebyshevCosine n θ = 0

Distinct normalized angular cosine modes are orthogonal over [0, π].

theorem TauCeti.integral_normalizedChebyshevCosine_mul_normalizedChebyshevCosine_eq_ite (m n : ℕ) : ∫ (θ : ℝ) in 0..Real.pi, normalizedChebyshevCosine m θ * normalizedChebyshevCosine n θ = if m = n then 1 else 0

Normalized angular Chebyshev-cosine orthogonality in Kronecker-delta form.