The weight ↔ measure isometry L²(w·μ) ≃ₗᵢ L²(μ)

For an almost-everywhere-positive real weight w on an arbitrary measurable space, multiplication by √w is a linear isometric equivalence from the weighted L² space L²(w·μ) onto L²(μ), where w·μ := μ.withDensity (ENNReal.ofReal ∘ w). It is an equivalence precisely because w > 0 almost everywhere: the inverse is multiplication by (√w)⁻¹.

This is the Part 0 primitive weightL2Isometry from the OrthogonalL2Bases roadmap, the single map converting a weight-in-the-measure normalization to a weight-in-the-function normalization. Once combined with HilbertBasis.mapₗᵢ (transport of a Hilbert basis across a ≃ₗᵢ, already in TauCeti.Analysis.InnerProductSpace.HilbertBasis.Map), it moves an orthogonal-polynomial basis of a weighted measure to the √w-envelope basis of the reference measure and back.

The construction is purely measure-theoretic, so it is stated over an arbitrary MeasurableSpace; only the later polynomial-facing layers specialize to Measure ℝ.

Main definitions

• TauCeti.weightL2Isometry — the isometric equivalence L²(w·μ) ≃ₗᵢ[𝕜] L²(μ).

Main statements

• TauCeti.weightL2Isometry_apply — the forward map is multiplication by √w.
• TauCeti.weightL2Isometry_symm_apply — the inverse map is multiplication by (√w)⁻¹.

The file also provides the underlying L² seminorm identity: the L²(μ) seminorm of √w · g equals the L²(w·μ) seminorm of g.

noncomputable def TauCeti.weightL2Isometry {𝕜 : Type u_1} [RCLike 𝕜] {α : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (w : α → ℝ) (hwpos : ∀ᵐ (x : α) ∂μ, 0 < w x) (hwm : AEMeasurable w μ) : ↥(MeasureTheory.Lp 𝕜 2 (μ.withDensity fun (x : α) => ENNReal.ofReal (w x))) ≃ₗᵢ[𝕜] ↥(MeasureTheory.Lp 𝕜 2 μ)

The weight ↔ measure isometry. For an almost-everywhere-positive weight w, multiplication by √w is a linear isometric equivalence L²(w·μ) ≃ₗᵢ[𝕜] L²(μ).

Equations

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

theorem TauCeti.weightL2Isometry_apply {𝕜 : Type u_1} [RCLike 𝕜] {α : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (w : α → ℝ) (hwpos : ∀ᵐ (x : α) ∂μ, 0 < w x) (hwm : AEMeasurable w μ) (f : ↥(MeasureTheory.Lp 𝕜 2 (μ.withDensity fun (x : α) => ENNReal.ofReal (w x)))) : ↑↑((weightL2Isometry μ w hwpos hwm) f) =ᵐ[μ] fun (x : α) => √(w x) • ↑↑f x

The forward isometry is multiplication by √w.

theorem TauCeti.weightL2Isometry_symm_apply {𝕜 : Type u_1} [RCLike 𝕜] {α : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (w : α → ℝ) (hwpos : ∀ᵐ (x : α) ∂μ, 0 < w x) (hwm : AEMeasurable w μ) (g : ↥(MeasureTheory.Lp 𝕜 2 μ)) : ↑↑((weightL2Isometry μ w hwpos hwm).symm g) =ᵐ[μ] fun (x : α) => (√(w x))⁻¹ • ↑↑g x

The inverse isometry is multiplication by (√w)⁻¹.