Integrability and L² membership of polynomials against a finite-moment measure

This file proves that a real polynomial, evaluated pointwise, is integrable and square-integrable against any measure on ℝ all of whose polynomial moments are finite:

• integrable_eval_of_forall_integrable_pow — a polynomial is integrable, being a finite linear combination of monomials;
• memLp_two_eval_of_forall_integrable_pow — a polynomial is in L², since the square of a polynomial is again a polynomial (hence integrable), and memLp_two_iff_integrable_sq.

Both consume only the moment hypothesis ∀ k, Integrable (x ↦ xᵏ) μ, with no dependence on the particular measure, so they apply verbatim to the Gaussian measure (all moments finite by Fernique) and to the compactly supported Chebyshev measure alike.

Building on the L² membership, polynomialEvalLp bundles polynomial evaluation, cast into any [RCLike 𝕜] scalar field, as an ℝ-linear map ℝ[X] →ₗ[ℝ] Lp 𝕜 2 μ. Being measure- and scalar-generic, it is the shared construction underlying the Gaussian and Chebyshev orthogonal-basis targets.

theorem TauCeti.integrable_eval_of_forall_integrable_pow {μ : MeasureTheory.Measure ℝ} (hmom : ∀ (k : ℕ), MeasureTheory.Integrable (fun (x : ℝ) => x ^ k) μ) (q : Polynomial ℝ) : MeasureTheory.Integrable (fun (x : ℝ) => Polynomial.eval x q) μ

A real polynomial is integrable against any measure all of whose polynomial moments are finite. The polynomial is a finite linear combination of the monomials x ↦ xᵏ, each integrable by hypothesis.

theorem TauCeti.memLp_two_eval_of_forall_integrable_pow {μ : MeasureTheory.Measure ℝ} (hmom : ∀ (k : ℕ), MeasureTheory.Integrable (fun (x : ℝ) => x ^ k) μ) (q : Polynomial ℝ) : MeasureTheory.MemLp (fun (x : ℝ) => Polynomial.eval x q) 2 μ

A real polynomial is in L² against any measure all of whose polynomial moments are finite. The square of a polynomial is again a polynomial, hence integrable by integrable_eval_of_forall_integrable_pow, and L² membership is integrability of the square.

theorem TauCeti.memLp_two_algebraMap_eval_of_forall_integrable_pow {μ : MeasureTheory.Measure ℝ} {𝕜 : Type u_1} [RCLike 𝕜] (hmom : ∀ (k : ℕ), MeasureTheory.Integrable (fun (x : ℝ) => x ^ k) μ) (q : Polynomial ℝ) : MeasureTheory.MemLp (fun (x : ℝ) => (algebraMap ℝ 𝕜) (Polynomial.eval x q)) 2 μ

A real polynomial evaluation, cast into any RCLike scalar field, lies in L² against any measure all of whose polynomial moments are finite.

noncomputable def TauCeti.polynomialEvalLp {μ : MeasureTheory.Measure ℝ} (𝕜 : Type u_1) [RCLike 𝕜] (hmom : ∀ (k : ℕ), MeasureTheory.Integrable (fun (x : ℝ) => x ^ k) μ) : Polynomial ℝ →ₗ[ℝ] ↥(MeasureTheory.Lp 𝕜 2 μ)

Polynomial evaluation, cast into any RCLike scalar field, bundled as an ℝ-linear map into L² against any measure all of whose polynomial moments are finite.

Equations

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

theorem TauCeti.coeFn_polynomialEvalLp {μ : MeasureTheory.Measure ℝ} (𝕜 : Type u_1) [RCLike 𝕜] (hmom : ∀ (k : ℕ), MeasureTheory.Integrable (fun (x : ℝ) => x ^ k) μ) (q : Polynomial ℝ) : ↑↑((polynomialEvalLp 𝕜 hmom) q) =ᵐ[μ] fun (x : ℝ) => (algebraMap ℝ 𝕜) (Polynomial.eval x q)

The L² representative of polynomialEvalLp is the expected scalar-cast pointwise evaluation.