Finite measure API for the Chebyshev T weight

This file records the finite-measure bookkeeping for Mathlib's Chebyshev orthogonality measure Polynomial.Chebyshev.measureT, together with the single normalization constant used by the roadmap's Chebyshev Hilbert-basis target.

The main facts are that measureT has total mass π, hence is finite and nonzero, that it is Lebesgue measure on (-1, 1] weighted by the Chebyshev weight w x = (1-x²)^{-1/2}, and that the existing Mathlib orthogonality lemmas combine into one Kronecker-delta statement with squared norms π in degree zero and π / 2 in positive degree. The file also records L² membership of the normalized T modes and the finite exponential moments used by the later Chebyshev Hilbert-basis construction.

For finite-coordinate arguments, use orthonormal_normalizedChebyshevTLp together with Mathlib's generic Orthonormal coordinate and finite linear combination API. This file intentionally keeps the Chebyshev-specific surface to the normalized modes and their orthonormality.

theorem TauCeti.chebyshevMeasureT_univ : Polynomial.Chebyshev.measureT Set.univ = ENNReal.ofReal Real.pi

The Chebyshev T orthogonality measure has total mass π.

instance TauCeti.chebyshevMeasureT.instIsFiniteMeasure : MeasureTheory.IsFiniteMeasure Polynomial.Chebyshev.measureT

Mathlib's Chebyshev T orthogonality measure is finite.

theorem TauCeti.chebyshevMeasureT_univ_pos : 0 < Polynomial.Chebyshev.measureT Set.univ

The Chebyshev T orthogonality measure has positive total mass.

theorem TauCeti.chebyshevMeasureT_ne_zero : Polynomial.Chebyshev.measureT ≠ 0

Mathlib's Chebyshev T orthogonality measure is nonzero.

The Chebyshev weight and the weighted Lebesgue measure

theorem TauCeti.measurable_chebyshevWeight : Measurable fun (x : ℝ) => √(1 - x ^ 2)⁻¹

The Chebyshev weight (1-x²)^{-1/2} is measurable.

theorem TauCeti.ae_zero_lt_chebyshevWeight : ∀ᵐ (x : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (-1) 1), 0 < √(1 - x ^ 2)⁻¹

The Chebyshev weight is almost everywhere positive on (-1, 1]: the endpoint 1, where 1 - x² vanishes, is a Lebesgue null set, so the interior bound x² < 1 holds almost everywhere.

instance TauCeti.chebyshevWeightedVolume.instIsFiniteMeasure : MeasureTheory.IsFiniteMeasure ((MeasureTheory.volume.restrict (Set.Ioc (-1) 1)).withDensity fun (x : ℝ) => ENNReal.ofReal √(1 - x ^ 2)⁻¹)

The weighted Lebesgue measure w · (volume|_{(-1,1]}) is finite: its total mass is the integral of the weight over a bounded interval, which Mathlib's Polynomial.Chebyshev.intervalIntegrable_sqrt_one_sub_sq_inv supplies.

theorem TauCeti.chebyshevMeasureT_eq_withDensity : Polynomial.Chebyshev.measureT = (MeasureTheory.volume.restrict (Set.Ioc (-1) 1)).withDensity fun (x : ℝ) => ENNReal.ofReal √(1 - x ^ 2)⁻¹

The Chebyshev measure is Lebesgue measure on (-1, 1] weighted by (1-x²)^{-1/2}.

Mathlib defines Polynomial.Chebyshev.measureT this way but does not expose the definition, so the identity has to be recovered from the public integral formula Polynomial.Chebyshev.integral_measureT. Both measures are finite, and a finite Borel measure on ℝ is determined by the integrals of bounded continuous functions (MeasureTheory.ext_of_forall_integral_eq_of_IsFiniteMeasure).

This is what lets TauCeti.weightL2Isometry — whose domain is spelled L²(μ.withDensity …) — be applied to L²(measureT).

theorem TauCeti.volume_restrict_absolutelyContinuous_measureT : (MeasureTheory.volume.restrict (Set.Ioc (-1) 1)).AbsolutelyContinuous Polynomial.Chebyshev.measureT

Lebesgue measure on (-1, 1] is absolutely continuous with respect to the Chebyshev measure: the weight is almost everywhere positive there, so weighting by it destroys no null sets. This is what moves an almost-everywhere identity between representatives from measureT to dx.

noncomputable def TauCeti.chebyshevTNormSq (n : ℕ) : ℝ

The squared L²(measureT) norm of the nth Chebyshev T polynomial.

Equations

• TauCeti.chebyshevTNormSq n = if n = 0 then Real.pi else Real.pi / 2

@[simp]

theorem TauCeti.chebyshevTNormSq_zero : chebyshevTNormSq 0 = Real.pi

@[simp]

theorem TauCeti.chebyshevTNormSq_of_ne_zero {n : ℕ} (hn : n ≠ 0) : chebyshevTNormSq n = Real.pi / 2

theorem TauCeti.chebyshevTNormSq_pos (n : ℕ) : 0 < chebyshevTNormSq n

The squared norm constant for Chebyshev T polynomials is positive.

theorem TauCeti.chebyshevTNormSq_ne_zero (n : ℕ) : chebyshevTNormSq n ≠ 0

The squared norm constant for Chebyshev T polynomials is nonzero.

theorem TauCeti.integral_eval_T_real_mul_self_measureT (n : ℕ) : ∫ (x : ℝ), Polynomial.eval x (Polynomial.Chebyshev.T ℝ ↑n) * Polynomial.eval x (Polynomial.Chebyshev.T ℝ ↑n) ∂Polynomial.Chebyshev.measureT = chebyshevTNormSq n

The diagonal Chebyshev T orthogonality integral, with the degree-zero and positive-degree cases hidden behind one normalization constant.

theorem TauCeti.integral_eval_T_real_mul_eval_T_real_measureT_eq_ite (m n : ℕ) : ∫ (x : ℝ), Polynomial.eval x (Polynomial.Chebyshev.T ℝ ↑m) * Polynomial.eval x (Polynomial.Chebyshev.T ℝ ↑n) ∂Polynomial.Chebyshev.measureT = if m = n then chebyshevTNormSq n else 0

Chebyshev T orthogonality in the Kronecker-delta form expected by the general orthogonality-to-Hilbert-basis bridge.

Exponential-moment consumer forms

theorem TauCeti.ae_mem_Icc_measureT : ∀ᵐ (x : ℝ) ∂Polynomial.Chebyshev.measureT, x ∈ Set.Icc (-1) 1

The Chebyshev T orthogonality measure is supported on [-1, 1].

theorem TauCeti.integrable_exp_mul_abs_smul_measureT {𝕜 : Type u_1} {β : Type u_2} [RCLike 𝕜] [NormedAddCommGroup β] [NormedSpace 𝕜 β] {g : ℝ → β} (a : ℝ) (hg : MeasureTheory.Integrable g Polynomial.Chebyshev.measureT) : MeasureTheory.Integrable (fun (x : ℝ) => ↑(Real.exp (a * |x|)) • g x) Polynomial.Chebyshev.measureT

Multiplication by an exponential absolute moment preserves L¹(measureT).

This is the compact-support consumer form used by the Chebyshev completeness argument.

L² consumer forms

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

The real normalized Chebyshev T mode, with squared norm one in L²(measureT).

Equations

• TauCeti.normalizedChebyshevT n x = Polynomial.eval x (Polynomial.Chebyshev.T ℝ ↑n) / √(TauCeti.chebyshevTNormSq n)

@[simp]

theorem TauCeti.normalizedChebyshevT_def (n : ℕ) (x : ℝ) : normalizedChebyshevT n x = Polynomial.eval x (Polynomial.Chebyshev.T ℝ ↑n) / √(chebyshevTNormSq n)

The defining equation for the real normalized Chebyshev T mode.

theorem TauCeti.continuous_normalizedChebyshevT (n : ℕ) : Continuous (normalizedChebyshevT n)

The real normalized Chebyshev T mode is continuous.

theorem TauCeti.memLp_normalizedChebyshevT_measureT (n : ℕ) : MeasureTheory.MemLp (normalizedChebyshevT n) 2 Polynomial.Chebyshev.measureT

The real normalized Chebyshev T mode lies in L²(measureT).

theorem TauCeti.memLp_algebraMap_normalizedChebyshevT_measureT {𝕜 : Type u_1} [RCLike 𝕜] (n : ℕ) : MeasureTheory.MemLp (fun (x : ℝ) => (algebraMap ℝ 𝕜) (normalizedChebyshevT n x)) 2 Polynomial.Chebyshev.measureT

The scalar-cast normalized Chebyshev T mode lies in L²(measureT), in the form consumed by the family-generic orthogonality-to-Hilbert-basis bridge.

noncomputable def TauCeti.normalizedChebyshevTLp (𝕜 : Type u_1) [RCLike 𝕜] (n : ℕ) : ↥(MeasureTheory.Lp 𝕜 2 Polynomial.Chebyshev.measureT)

The normalized Chebyshev T mode as a vector of L²(measureT).

Equations

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

theorem TauCeti.coeFn_normalizedChebyshevTLp {𝕜 : Type u_1} [RCLike 𝕜] (n : ℕ) : ↑↑(normalizedChebyshevTLp 𝕜 n) =ᵐ[Polynomial.Chebyshev.measureT] fun (x : ℝ) => (algebraMap ℝ 𝕜) (normalizedChebyshevT n x)

The Lp representative of the normalized Chebyshev T mode is the expected scalar-cast function.

@[simp]

theorem TauCeti.integral_normalizedChebyshevT_mul_normalizedChebyshevT_measureT_eq_ite (m n : ℕ) : ∫ (x : ℝ), normalizedChebyshevT m x * normalizedChebyshevT n x ∂Polynomial.Chebyshev.measureT = if m = n then 1 else 0

The real measureT integral of two normalized Chebyshev T modes is the Kronecker delta.

@[simp]

theorem TauCeti.inner_normalizedChebyshevTLp {𝕜 : Type u_1} [RCLike 𝕜] (m n : ℕ) : inner 𝕜 (normalizedChebyshevTLp 𝕜 m) (normalizedChebyshevTLp 𝕜 n) = if m = n then 1 else 0

The normalized Chebyshev T modes have Kronecker-delta inner products in L²(measureT).

theorem TauCeti.inner_normalizedChebyshevTLp_real (m n : ℕ) : inner ℝ (normalizedChebyshevTLp ℝ m) (normalizedChebyshevTLp ℝ n) = if m = n then 1 else 0

The normalized Chebyshev T modes have Kronecker-delta inner products in real L²(measureT).

theorem TauCeti.orthonormal_normalizedChebyshevTLp {𝕜 : Type u_1} [RCLike 𝕜] : Orthonormal 𝕜 (normalizedChebyshevTLp 𝕜)

The normalized Chebyshev T modes form an orthonormal family in L²(measureT).

theorem TauCeti.orthonormal_normalizedChebyshevTLp_real : Orthonormal ℝ (normalizedChebyshevTLp ℝ)

The normalized Chebyshev T modes form an orthonormal family in real L²(measureT).