From an orthogonality relation to a Hilbert basis of a weighted measure

Given a family of real-valued functions f : ℕ → α → ℝ, an almost-everywhere-positive weight w : α → ℝ, and positive normalization constants c : ℕ → ℝ satisfying the orthogonality relation ∫ f m x * f n x * w x ∂μ = if m = n then c n else 0, the normalized functions fₙ/√cₙ, viewed as elements of the weighted L² space L²(w·μ) (with w·μ := μ.withDensity (ENNReal.ofReal ∘ w)), form an orthonormal family; if in addition their span has trivial orthogonal complement, they form a HilbertBasis.

This is the family-agnostic assembly step of Part B2 of the OrthogonalL2Bases roadmap: the orthogonality relation and the completeness hypothesis enter as arguments, so the bridge is grounded by construction and reusable across families. The canonical application is a family of orthogonal polynomials f n := (p n).eval (Hermite, Chebyshev, ...), but any orthogonal system of real-valued functions (e.g. trigonometric) fits the same bridge. The scalars are generic over [RCLike 𝕜]: the real function values are cast through algebraMap ℝ 𝕜, so a single construction serves both the real and complex L² spaces.

Two normalizations come out of one construction. The bare normalized functions are natively an orthonormal basis of the weighted measure L²(w·μ) (hilbertBasisOfWeightedMeasure); pushing that basis across the weightL2Isometry (multiplication by √w) yields the √w-envelope basis of the reference measure L²(μ) (hilbertBasisOfOrthogonalSystem), with no separate proof. Each basis exports its element-level coe_* lemma, so downstream family instances specialize rather than re-derive.

Main definitions

• TauCeti.bareNormalizedLp — the normalized function fₙ/√cₙ as a vector of L²(w·μ; 𝕜).
• TauCeti.hilbertBasisOfWeightedMeasure — the bare functions as a HilbertBasis of L²(w·μ).
• TauCeti.hilbertBasisOfOrthogonalSystem — the √w-envelope basis of L²(μ), the weightL2Isometry-image of the weighted-measure basis.

Main statements

• TauCeti.orthonormal_bareNormalizedLp — orthonormality from the orthogonality relation.
• TauCeti.coe_hilbertBasisOfWeightedMeasure, TauCeti.coe_hilbertBasisOfOrthogonalSystem — the element-level characterizations (anti-vacuity pins).
• TauCeti.coeFn_hilbertBasisOfOrthogonalSystem — the envelope basis vector as the explicit function fₙ·√w/√cₙ, the form a family instance identifies with its own envelope family.

noncomputable def TauCeti.bareNormalizedLp {𝕜 : Type u_1} [RCLike 𝕜] {α : Type u_2} [MeasurableSpace α] (f : ℕ → α → ℝ) (w : α → ℝ) (c : ℕ → ℝ) {μ : MeasureTheory.Measure α} (hmem : ∀ (n : ℕ), MeasureTheory.MemLp (fun (x : α) => (algebraMap ℝ 𝕜) (f n x / √(c n))) 2 (μ.withDensity fun (x : α) => ENNReal.ofReal (w x))) (n : ℕ) : ↥(MeasureTheory.Lp 𝕜 2 (μ.withDensity fun (x : α) => ENNReal.ofReal (w x)))

The bare normalized function fₙ/√cₙ as an element of L²(w·μ; 𝕜), where w·μ = μ.withDensity (ENNReal.ofReal ∘ w) and the real value is cast through algebraMap ℝ 𝕜.

Equations

• TauCeti.bareNormalizedLp f w c hmem n = MeasureTheory.MemLp.toLp (fun (x : α) => (algebraMap ℝ 𝕜) (f n x / √(c n))) ⋯

theorem TauCeti.coeFn_bareNormalizedLp {𝕜 : Type u_1} [RCLike 𝕜] {α : Type u_2} [MeasurableSpace α] (f : ℕ → α → ℝ) (w : α → ℝ) (c : ℕ → ℝ) {μ : MeasureTheory.Measure α} (hmem : ∀ (n : ℕ), MeasureTheory.MemLp (fun (x : α) => (algebraMap ℝ 𝕜) (f n x / √(c n))) 2 (μ.withDensity fun (x : α) => ENNReal.ofReal (w x))) (n : ℕ) : ↑↑(bareNormalizedLp f w c hmem n) =ᵐ[μ.withDensity fun (x : α) => ENNReal.ofReal (w x)] fun (x : α) => (algebraMap ℝ 𝕜) (f n x / √(c n))

The Lp representative of bareNormalizedLp is the expected scalar-cast normalized function.

theorem TauCeti.inner_bareNormalizedLp {𝕜 : Type u_1} [RCLike 𝕜] {α : Type u_2} [MeasurableSpace α] (f : ℕ → α → ℝ) (w : α → ℝ) (c : ℕ → ℝ) {μ : MeasureTheory.Measure α} (hwnn : ∀ᵐ (x : α) ∂μ, 0 ≤ w x) (hwm : AEMeasurable w μ) (hc : ∀ (n : ℕ), 0 < c n) (horth : ∀ (m n : ℕ), ∫ (x : α), f m x * f n x * w x ∂μ = if m = n then c n else 0) (hmem : ∀ (n : ℕ), MeasureTheory.MemLp (fun (x : α) => (algebraMap ℝ 𝕜) (f n x / √(c n))) 2 (μ.withDensity fun (x : α) => ENNReal.ofReal (w x))) (m n : ℕ) : inner 𝕜 (bareNormalizedLp f w c hmem m) (bareNormalizedLp f w c hmem n) = if m = n then 1 else 0

The normalized bare functions have Kronecker-delta inner products in L²(w·μ).

theorem TauCeti.orthonormal_bareNormalizedLp {𝕜 : Type u_1} [RCLike 𝕜] {α : Type u_2} [MeasurableSpace α] (f : ℕ → α → ℝ) (w : α → ℝ) (c : ℕ → ℝ) {μ : MeasureTheory.Measure α} (hwnn : ∀ᵐ (x : α) ∂μ, 0 ≤ w x) (hwm : AEMeasurable w μ) (hc : ∀ (n : ℕ), 0 < c n) (horth : ∀ (m n : ℕ), ∫ (x : α), f m x * f n x * w x ∂μ = if m = n then c n else 0) (hmem : ∀ (n : ℕ), MeasureTheory.MemLp (fun (x : α) => (algebraMap ℝ 𝕜) (f n x / √(c n))) 2 (μ.withDensity fun (x : α) => ENNReal.ofReal (w x))) : Orthonormal 𝕜 (bareNormalizedLp f w c hmem)

Orthonormality from the orthogonality relation. The normalized bare functions fₙ/√cₙ form an orthonormal family in L²(w·μ).

noncomputable def TauCeti.hilbertBasisOfWeightedMeasure {𝕜 : Type u_1} [RCLike 𝕜] {α : Type u_2} [MeasurableSpace α] (f : ℕ → α → ℝ) (w : α → ℝ) (c : ℕ → ℝ) {μ : MeasureTheory.Measure α} (hwnn : ∀ᵐ (x : α) ∂μ, 0 ≤ w x) (hwm : AEMeasurable w μ) (hc : ∀ (n : ℕ), 0 < c n) (horth : ∀ (m n : ℕ), ∫ (x : α), f m x * f n x * w x ∂μ = if m = n then c n else 0) (hmem : ∀ (n : ℕ), MeasureTheory.MemLp (fun (x : α) => (algebraMap ℝ 𝕜) (f n x / √(c n))) 2 (μ.withDensity fun (x : α) => ENNReal.ofReal (w x))) (hcomplete : (Submodule.span 𝕜 (Set.range (bareNormalizedLp f w c hmem)))ᗮ = ⊥) : HilbertBasis ℕ 𝕜 ↥(MeasureTheory.Lp 𝕜 2 (μ.withDensity fun (x : α) => ENNReal.ofReal (w x)))

The weighted-measure basis. The normalized bare functions, orthonormal by the orthogonality relation and complete by hypothesis, form a Hilbert basis of L²(w·μ) — the textbook statement that a family of orthogonal functions is an orthonormal basis of its own weighted L² space.

Equations

• TauCeti.hilbertBasisOfWeightedMeasure f w c hwnn hwm hc horth hmem hcomplete = HilbertBasis.mkOfOrthogonalEqBot ⋯ hcomplete

theorem TauCeti.coe_hilbertBasisOfWeightedMeasure {𝕜 : Type u_1} [RCLike 𝕜] {α : Type u_2} [MeasurableSpace α] (f : ℕ → α → ℝ) (w : α → ℝ) (c : ℕ → ℝ) {μ : MeasureTheory.Measure α} (hwnn : ∀ᵐ (x : α) ∂μ, 0 ≤ w x) (hwm : AEMeasurable w μ) (hc : ∀ (n : ℕ), 0 < c n) (horth : ∀ (m n : ℕ), ∫ (x : α), f m x * f n x * w x ∂μ = if m = n then c n else 0) (hmem : ∀ (n : ℕ), MeasureTheory.MemLp (fun (x : α) => (algebraMap ℝ 𝕜) (f n x / √(c n))) 2 (μ.withDensity fun (x : α) => ENNReal.ofReal (w x))) (hcomplete : (Submodule.span 𝕜 (Set.range (bareNormalizedLp f w c hmem)))ᗮ = ⊥) : ⇑(hilbertBasisOfWeightedMeasure f w c hwnn hwm hc horth hmem hcomplete) = bareNormalizedLp f w c hmem

Element-level characterization of the weighted-measure basis.

noncomputable def TauCeti.hilbertBasisOfOrthogonalSystem {𝕜 : Type u_1} [RCLike 𝕜] {α : Type u_2} [MeasurableSpace α] (f : ℕ → α → ℝ) (w : α → ℝ) (c : ℕ → ℝ) {μ : MeasureTheory.Measure α} (hwpos : ∀ᵐ (x : α) ∂μ, 0 < w x) (hwm : AEMeasurable w μ) (hc : ∀ (n : ℕ), 0 < c n) (horth : ∀ (m n : ℕ), ∫ (x : α), f m x * f n x * w x ∂μ = if m = n then c n else 0) (hmem : ∀ (n : ℕ), MeasureTheory.MemLp (fun (x : α) => (algebraMap ℝ 𝕜) (f n x / √(c n))) 2 (μ.withDensity fun (x : α) => ENNReal.ofReal (w x))) (hcomplete : (Submodule.span 𝕜 (Set.range (bareNormalizedLp f w c hmem)))ᗮ = ⊥) : HilbertBasis ℕ 𝕜 ↥(MeasureTheory.Lp 𝕜 2 μ)

The √w-envelope basis of L²(μ). The weightL2Isometry-image (multiplication by √w) of the weighted-measure basis; the √w-normalized functions fₙ·√w/√cₙ form a Hilbert basis of the reference measure L²(μ), obtained with no separate proof.

Equations

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

theorem TauCeti.coe_hilbertBasisOfOrthogonalSystem {𝕜 : Type u_1} [RCLike 𝕜] {α : Type u_2} [MeasurableSpace α] (f : ℕ → α → ℝ) (w : α → ℝ) (c : ℕ → ℝ) {μ : MeasureTheory.Measure α} (hwpos : ∀ᵐ (x : α) ∂μ, 0 < w x) (hwm : AEMeasurable w μ) (hc : ∀ (n : ℕ), 0 < c n) (horth : ∀ (m n : ℕ), ∫ (x : α), f m x * f n x * w x ∂μ = if m = n then c n else 0) (hmem : ∀ (n : ℕ), MeasureTheory.MemLp (fun (x : α) => (algebraMap ℝ 𝕜) (f n x / √(c n))) 2 (μ.withDensity fun (x : α) => ENNReal.ofReal (w x))) (hcomplete : (Submodule.span 𝕜 (Set.range (bareNormalizedLp f w c hmem)))ᗮ = ⊥) (n : ℕ) : (hilbertBasisOfOrthogonalSystem f w c hwpos hwm hc horth hmem hcomplete) n = (weightL2Isometry μ w hwpos hwm) (bareNormalizedLp f w c hmem n)

Element-level characterization of the √w-envelope basis: the weightL2Isometry-image of the weighted-measure basis vector.

theorem TauCeti.coeFn_hilbertBasisOfOrthogonalSystem {𝕜 : Type u_1} [RCLike 𝕜] {α : Type u_2} [MeasurableSpace α] (f : ℕ → α → ℝ) (w : α → ℝ) (c : ℕ → ℝ) {μ : MeasureTheory.Measure α} (hwpos : ∀ᵐ (x : α) ∂μ, 0 < w x) (hwm : AEMeasurable w μ) (hc : ∀ (n : ℕ), 0 < c n) (horth : ∀ (m n : ℕ), ∫ (x : α), f m x * f n x * w x ∂μ = if m = n then c n else 0) (hmem : ∀ (n : ℕ), MeasureTheory.MemLp (fun (x : α) => (algebraMap ℝ 𝕜) (f n x / √(c n))) 2 (μ.withDensity fun (x : α) => ENNReal.ofReal (w x))) (hcomplete : (Submodule.span 𝕜 (Set.range (bareNormalizedLp f w c hmem)))ᗮ = ⊥) (n : ℕ) : ↑↑((hilbertBasisOfOrthogonalSystem f w c hwpos hwm hc horth hmem hcomplete) n) =ᵐ[μ] fun (x : α) => (algebraMap ℝ 𝕜) (f n x * √(w x) / √(c n))

The envelope basis vectors are the functions fₙ·√w/√cₙ. Where TauCeti.coe_hilbertBasisOfOrthogonalSystem names the n-th vector as a weightL2Isometry image, this multiplies that image out, so a family instance can identify the vector with its own envelope family by pointwise algebra alone.

Positivity of w is what makes the statement μ-almost-everywhere rather than merely w·μ-almost-everywhere: it makes μ absolutely continuous with respect to w·μ, so the representative of the weighted-measure basis vector may be read on μ as well.