Completeness of an orthogonal polynomial system from moment determinacy

TauCeti.hilbertBasisOfWeightedMeasure assembles a HilbertBasis of L²(w·μ) from an orthogonality relation and a completeness hypothesis (span …)ᗮ = ⊥, but nothing in the library discharges that hypothesis. This file supplies it for a family of polynomials of exact degree, the case every classical orthogonal family falls under.

The mechanism is moment determinacy. If the weighted measure w·μ carries one finite exponential moment then TauCeti.ae_eq_zero_of_forall_moment_eq_zero_of_exists_integrable_exp says a g ∈ L²(w·μ) orthogonal to every monomial vanishes. So the only thing completeness needs of the family is that it spans ℝ[X], and that is the hypothesis the core theorem takes.

Exact degrees are one sufficient route to spanning, not the content of the argument: a family with (p n).degree = n spans, because over a field every nonzero leading coefficient is a unit (Polynomial.Sequence.span). That case is kept as a corollary, since it is the one every classical orthogonal family satisfies. Requiring degree rather than natDegree matters there: natDegree 0 = 0 would admit p 0 = 0, which silently destroys the basis.

Main statements

• TauCeti.memLp_two_algebraMap_eval — polynomials lie in L² of a measure carrying one finite exponential moment, via TauCeti.integrable_pow_of_exp_moment.
• TauCeti.memLp_two_bareNormalized — the normalized-family MemLp obligation, discharged from that same exponential moment so callers need not repeat it.
• TauCeti.orthogonal_span_range_bareNormalizedLp_eq_bot_of_span_eq_top — the completeness input of the B2 bridge, from spanning alone.
• TauCeti.orthogonal_span_range_bareNormalizedLp_eq_bot — its exact-degree specialization.

theorem TauCeti.memLp_two_algebraMap_eval {𝕜 : Type u_1} [RCLike 𝕜] {ν : MeasureTheory.Measure ℝ} (hexp : ∃ (a : ℝ), 0 < a ∧ MeasureTheory.Integrable (fun (x : ℝ) => Real.exp (a * |x|)) ν) (q : Polynomial ℝ) : MeasureTheory.MemLp (fun (x : ℝ) => (algebraMap ℝ 𝕜) (Polynomial.eval x q)) 2 ν

Every polynomial lies in L² of a measure carrying one finite exponential moment.

theorem TauCeti.memLp_two_algebraMap_eval_div {𝕜 : Type u_1} [RCLike 𝕜] {ν : MeasureTheory.Measure ℝ} (hexp : ∃ (a : ℝ), 0 < a ∧ MeasureTheory.Integrable (fun (x : ℝ) => Real.exp (a * |x|)) ν) (q : Polynomial ℝ) (r : ℝ) : MeasureTheory.MemLp (fun (x : ℝ) => (algebraMap ℝ 𝕜) (Polynomial.eval x q / r)) 2 ν

Dividing by a constant keeps a polynomial in L²: q/r is again the evaluation of a polynomial, namely C r⁻¹ * q. This also covers r = 0, where both sides are 0.

theorem TauCeti.memLp_two_bareNormalized {𝕜 : Type u_1} [RCLike 𝕜] {ν : MeasureTheory.Measure ℝ} (hexp : ∃ (a : ℝ), 0 < a ∧ MeasureTheory.Integrable (fun (x : ℝ) => Real.exp (a * |x|)) ν) (p : ℕ → Polynomial ℝ) (c : ℕ → ℝ) (n : ℕ) : MeasureTheory.MemLp (fun (x : ℝ) => (algebraMap ℝ 𝕜) (Polynomial.eval x (p n) / √(c n))) 2 ν

The MemLp obligation of TauCeti.bareNormalizedLp for a polynomial family, discharged from the one exponential moment that the completeness theorem already assumes. Supplied as the default value of that theorem's hmem argument, so callers do not repeat this proof.

theorem TauCeti.orthogonal_span_range_bareNormalizedLp_eq_bot_of_span_eq_top {𝕜 : Type u_1} [RCLike 𝕜] {μ : MeasureTheory.Measure ℝ} (p : ℕ → Polynomial ℝ) (w : ℝ → ℝ) (c : ℕ → ℝ) (hspan : Submodule.span ℝ (Set.range p) = ⊤) (hc : ∀ (n : ℕ), 0 < c n) (hexp : ∃ (a : ℝ), 0 < a ∧ MeasureTheory.Integrable (fun (x : ℝ) => Real.exp (a * |x|)) (μ.withDensity fun (x : ℝ) => ENNReal.ofReal (w x))) (hmem : ∀ (n : ℕ), MeasureTheory.MemLp (fun (x : ℝ) => (algebraMap ℝ 𝕜) (Polynomial.eval x (p n) / √(c n))) 2 (μ.withDensity fun (x : ℝ) => ENNReal.ofReal (w x)) := ⋯) : (Submodule.span 𝕜 (Set.range (bareNormalizedLp (fun (n : ℕ) (x : ℝ) => Polynomial.eval x (p n)) w c hmem)))ᗮ = ⊥

Roadmap B1 → B2 bridge: completeness of a spanning polynomial family.

If the weighted measure w·μ carries one finite exponential moment and p spans ℝ[X], then the normalized polynomials span a dense subspace of L²(w·μ) — the orthogonal complement of their span is trivial. This is the hcomplete input that TauCeti.hilbertBasisOfWeightedMeasure consumes.

Spanning is all the argument uses; see TauCeti.orthogonal_span_range_bareNormalizedLp_eq_bot for the exact-degree families that motivate it.

theorem TauCeti.orthogonal_span_range_bareNormalizedLp_eq_bot {𝕜 : Type u_1} [RCLike 𝕜] {μ : MeasureTheory.Measure ℝ} (p : ℕ → Polynomial ℝ) (w : ℝ → ℝ) (c : ℕ → ℝ) (hdeg : ∀ (n : ℕ), (p n).degree = ↑n) (hc : ∀ (n : ℕ), 0 < c n) (hexp : ∃ (a : ℝ), 0 < a ∧ MeasureTheory.Integrable (fun (x : ℝ) => Real.exp (a * |x|)) (μ.withDensity fun (x : ℝ) => ENNReal.ofReal (w x))) (hmem : ∀ (n : ℕ), MeasureTheory.MemLp (fun (x : ℝ) => (algebraMap ℝ 𝕜) (Polynomial.eval x (p n) / √(c n))) 2 (μ.withDensity fun (x : ℝ) => ENNReal.ofReal (w x)) := ⋯) : (Submodule.span 𝕜 (Set.range (bareNormalizedLp (fun (n : ℕ) (x : ℝ) => Polynomial.eval x (p n)) w c hmem)))ᗮ = ⊥

Completeness of an exact-degree polynomial family — the specialization of TauCeti.orthogonal_span_range_bareNormalizedLp_eq_bot_of_span_eq_top that every classical orthogonal family satisfies.

Exact degrees make p a Polynomial.Sequence, and over a field every nonzero leading coefficient is a unit, so p spans ℝ[X].