The Chebyshev envelope functions as a Hilbert basis of L²((-1, 1])

TauCeti.chebyshevTHilbertBasis carries the Chebyshev weight (1-x²)^{-1/2} in the measure: the bare normalized polynomials Tₙ/√cₙ are an orthonormal basis of L²(measureT). This file supplies the other normalization, with the weight in the function: the envelope functions

τₙ(x) = Tₙ(x)·(1-x²)^{-1/4}/√cₙ, c₀ = π, cₙ = π/2 for n ≠ 0,

are an orthonormal basis of L²((-1, 1]; dx) for plain Lebesgue measure on the Chebyshev interval. That is the basis a Chebyshev expansion taken in an unweighted L² runs against.

Both normalizations come out of the same family-agnostic bridge. The basis here is TauCeti.hilbertBasisOfOrthogonalSystem at μ = volume.restrict (Set.Ioc (-1) 1), w x = (1-x²)^{-1/2}, f n = (T ℝ n).eval and c = TauCeti.chebyshevTNormSq, so it exercises that bridge on a compact weighted measure rather than on the Gaussian. Its orthogonality input is Mathlib's, read off measureT through Polynomial.Chebyshev.integral_measureT; its completeness input is TauCeti.orthogonal_span_range_bareNormalizedLp_eq_bot, whose one analytic hypothesis — a finite exponential moment — is free on a bounded interval.

The reference measure is volume.restrict (Set.Ioc (-1) 1) rather than Mathlib's measureT itself. The two are related by TauCeti.chebyshevMeasureT_eq_withDensity, which is what identifies this basis with TauCeti.chebyshevTHilbertBasis through the weight-change isometry; the orthogonality relation needed here is read off the public integral formula directly, which is all the bridge asks for.

Main statements

• TauCeti.integral_eval_T_real_mul_eval_T_real_mul_chebyshevWeight — the Chebyshev orthogonality relation re-keyed to Lebesgue measure on (-1, 1], with the weight in the integrand.
• TauCeti.integrable_exp_mul_abs_chebyshevWeight — the weighted measure has every exponential moment finite, the hypothesis the completeness theorem needs.
• TauCeti.integral_chebyshevTEnvelope_mul_chebyshevTEnvelope — the envelope functions are orthonormal for dx on (-1, 1].
• TauCeti.chebyshevTEnvelopeHilbertBasis — the basis itself.
• TauCeti.coeFn_chebyshevTEnvelopeHilbertBasis, TauCeti.coe_chebyshevTEnvelopeHilbertBasis — the anti-vacuity pins: the n-th basis vector really is τₙ, almost everywhere and as an Lp vector.

The moments of the weight

theorem TauCeti.integrable_exp_mul_abs_chebyshevWeight (a : ℝ) : MeasureTheory.Integrable (fun (x : ℝ) => Real.exp (a * |x|)) ((MeasureTheory.volume.restrict (Set.Ioc (-1) 1)).withDensity fun (x : ℝ) => ENNReal.ofReal √(1 - x ^ 2)⁻¹)

Finite exponential moments of the Chebyshev weight. For every rate a the function e^{a|x|} is integrable against the weighted measure w·(volume|_{(-1,1]}). The measure lives on a bounded interval, so this is the bounded-support principle MeasureTheory.Integrable.exp_abs_smul_of_ae_abs_le applied to integrability of the weight itself, which is Mathlib's Polynomial.Chebyshev.intervalIntegrable_sqrt_one_sub_sq_inv.

This is the single analytic hypothesis behind both the L² membership of the polynomials and the completeness of the family.

theorem TauCeti.integral_eval_T_real_mul_eval_T_real_mul_chebyshevWeight (m n : ℕ) : ∫ (x : ℝ) in Set.Ioc (-1) 1, Polynomial.eval x (Polynomial.Chebyshev.T ℝ ↑m) * Polynomial.eval x (Polynomial.Chebyshev.T ℝ ↑n) * √(1 - x ^ 2)⁻¹ = if m = n then chebyshevTNormSq n else 0

The Chebyshev orthogonality relation on Lebesgue measure. Mathlib's relation is stated against measureT; Polynomial.Chebyshev.integral_measureT rewrites it as an interval integral, which is exactly an integral against volume.restrict (Set.Ioc (-1) 1) with the weight moved into the integrand — the shape TauCeti.hilbertBasisOfOrthogonalSystem consumes.

The envelope functions

noncomputable def TauCeti.chebyshevTEnvelope (n : ℕ) (x : ℝ) : ℝ

The n-th Chebyshev envelope function τₙ(x) = Tₙ(x)·(1-x²)^{-1/4}/√cₙ: the normalized Chebyshev mode TauCeti.normalizedChebyshevT multiplied by the square root of the Chebyshev weight, which is the weight-in-the-function counterpart of that mode.

Equations

• TauCeti.chebyshevTEnvelope n x = TauCeti.normalizedChebyshevT n x * √√(1 - x ^ 2)⁻¹

@[simp]

theorem TauCeti.chebyshevTEnvelope_def (n : ℕ) (x : ℝ) : chebyshevTEnvelope n x = normalizedChebyshevT n x * √√(1 - x ^ 2)⁻¹

The defining equation for the Chebyshev envelope function.

theorem TauCeti.chebyshevTEnvelope_zero (x : ℝ) : chebyshevTEnvelope 0 x = √√(1 - x ^ 2)⁻¹ / √Real.pi

The zeroth envelope function is the bare square root of the weight, normalized by √π.

theorem TauCeti.integral_chebyshevTEnvelope_mul_chebyshevTEnvelope (m n : ℕ) : ∫ (x : ℝ) in Set.Ioc (-1) 1, chebyshevTEnvelope m x * chebyshevTEnvelope n x = if m = n then 1 else 0

The envelope functions are orthonormal for Lebesgue measure on (-1, 1]. Multiplying two envelope functions restores the full weight, √w·√w = w, which returns the integral to the weighted orthogonality relation.

The Hilbert basis

noncomputable def TauCeti.chebyshevTEnvelopeHilbertBasis (𝕜 : Type u_1) [RCLike 𝕜] : HilbertBasis ℕ 𝕜 ↥(MeasureTheory.Lp 𝕜 2 (MeasureTheory.volume.restrict (Set.Ioc (-1) 1)))

The Chebyshev envelope functions are a Hilbert basis of L²((-1, 1]; dx). The weight-in-the-function normalization of Part C of the OrthogonalL2Bases roadmap, assembled from the same bridge as the weight-in-the-measure basis TauCeti.chebyshevTHilbertBasis: orthonormality from the Chebyshev orthogonality relation, completeness from moment determinacy applied to the exact-degree family Tₙ.

Equations

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

theorem TauCeti.coeFn_chebyshevTEnvelopeHilbertBasis (𝕜 : Type u_1) [RCLike 𝕜] (n : ℕ) : ↑↑((chebyshevTEnvelopeHilbertBasis 𝕜) n) =ᵐ[MeasureTheory.volume.restrict (Set.Ioc (-1) 1)] fun (x : ℝ) => (algebraMap ℝ 𝕜) (chebyshevTEnvelope n x)

The basis vectors are the envelope functions. Without this the construction would only exhibit some Hilbert basis of L²((-1, 1]); here each vector is pinned to τₙ.

theorem TauCeti.memLp_two_algebraMap_chebyshevTEnvelope (𝕜 : Type u_1) [RCLike 𝕜] (n : ℕ) : MeasureTheory.MemLp (fun (x : ℝ) => (algebraMap ℝ 𝕜) (chebyshevTEnvelope n x)) 2 (MeasureTheory.volume.restrict (Set.Ioc (-1) 1))

Each envelope function lies in L²((-1, 1]; dx). It is the representative of a basis vector, so this is read off the basis rather than re-proved: the L² membership is exactly what the weighted MemLp obligation of the bridge already established, transported by TauCeti.coeFn_chebyshevTEnvelopeHilbertBasis.

noncomputable def TauCeti.chebyshevTEnvelopeLp (𝕜 : Type u_1) [RCLike 𝕜] (n : ℕ) : ↥(MeasureTheory.Lp 𝕜 2 (MeasureTheory.volume.restrict (Set.Ioc (-1) 1)))

The n-th envelope function as a vector of L²((-1, 1]; dx).

Equations

• TauCeti.chebyshevTEnvelopeLp 𝕜 n = MeasureTheory.MemLp.toLp (fun (x : ℝ) => (algebraMap ℝ 𝕜) (TauCeti.chebyshevTEnvelope n x)) ⋯

theorem TauCeti.coeFn_chebyshevTEnvelopeLp (𝕜 : Type u_1) [RCLike 𝕜] (n : ℕ) : ↑↑(chebyshevTEnvelopeLp 𝕜 n) =ᵐ[MeasureTheory.volume.restrict (Set.Ioc (-1) 1)] fun (x : ℝ) => (algebraMap ℝ 𝕜) (chebyshevTEnvelope n x)

The Lp representative of TauCeti.chebyshevTEnvelopeLp is the expected scalar-cast envelope function.

@[simp]

theorem TauCeti.coe_chebyshevTEnvelopeHilbertBasis (𝕜 : Type u_1) [RCLike 𝕜] : ⇑(chebyshevTEnvelopeHilbertBasis 𝕜) = chebyshevTEnvelopeLp 𝕜

The basis is the envelope family, as an equality of ℕ-indexed families of L² vectors. This is the shape the roadmap's element-level export asks for; it upgrades the almost-everywhere TauCeti.coeFn_chebyshevTEnvelopeHilbertBasis to an identity of Lp vectors.

theorem TauCeti.orthonormal_chebyshevTEnvelopeLp (𝕜 : Type u_1) [RCLike 𝕜] : Orthonormal 𝕜 (chebyshevTEnvelopeLp 𝕜)

The envelope functions are orthonormal in L²((-1, 1]; dx).