Imports
/- Copyright (c) 2026 Gregory J. Loges. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Gregory J. Loges -/ module public import Mathlib.Analysis.Calculus.BumpFunction.InnerProduct public import Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls public import Physlib.QuantumMechanics.HilbertSpaces.SpaceD.SchwartzSubmodule

Polynomially-bounded Schwartz submodules

i. Overview

In this module we define polynomially-bounded Schwartz submodules of SpaceDHilbertSpace d μ.

For each a : ℕ∞, PolyBddSchwartzSubmodule d a μ is the submodule corresponding to Schwartz maps f satisfying the polynomial growth bounds ‖x‖ ^ (-k) * ‖f x‖ ≤ Cₖ for all (k : ℕ) ≤ a. In particular, for a = ⊤ such a bound holds for all natural numbers.

These serve as a natural domain for singular unbounded operators. For example, the 1/r Coulomb potential operator maps PolyBddSchwartzSubmodule d ⊤ μ to itself. In the same way that multiplying a Schwartz map by any polynomial in the coordinates results in a square-integrable function, polynomially-bounded Schwartz maps may be multiplied by Laurent polynomials and remain square-integrable (the precise condition depends on d, a and the negative degree of the Laurent polynomial).

Note: the condition defining polynomially-bounded Schwartz maps is phrased as ‖x‖ ^ (-k) * ‖f x‖ ≤ Cₖ rather than as ‖f x‖ ≤ Cₖ * ‖x‖ ^ k to mirror SchwartzMap.decay. These two conditions only differ at x = 0 and are therefore equivalent for d > 0 since then f 0 may be determined by continuity. For d = 0 the former does not constrain f 0 = 0 (since x = 0 is the only point and 0⁻¹ = 0) while the latter does (and would therefore spoil their being dense in SpaceDHilbertSpace 0 ≅ ℂ).

ii. Key results

    PolyBddSchwartzSubmodule d (a : ℕ∞) μ: Restriction of SchwartzSubmodule d μ to those Schwartz maps which are bounded by powers of ‖x‖.

    PolyBddSchwartzSubmodule.dense: These submodules are dense in SpaceDHilbertSpace d μ.

iii. Table of contents

    A. Definitions

    B. Coercions

    C. (In)equalities

    D. Density

iv. References

@[expose] public section

A. Definitions

A function is a bounded Schwartz map if it is both Schwartz and bounded by powers of ‖x‖.

d:a:ℕ∞c:f:𝓢(Space d, )hf:f {f | (k : ), k a C, 0 < C (x : Space d), x ^ (-k) * f x C}k:hk:k aC:hC_pos:0 < ChC: (x : Space d), x ^ (-k) * f x Cx:Space dc * (x ^ (-k) * f x) (1 + c) * C exact le_trans (mul_le_mul_of_nonneg_left (hC x) (norm_nonneg c)) (d:a:ℕ∞c:f:𝓢(Space d, )hf:f {f | (k : ), k a C, 0 < C (x : Space d), x ^ (-k) * f x C}k:hk:k aC:hC_pos:0 < ChC: (x : Space d), x ^ (-k) * f x Cx:Space dc * C (1 + c) * C All goals completed! 🐙)

The continuous linear map schwartzIncl with domain restricted to PolyBddSchwartzMap d a.

def polyBddSchwartzIncl {d : } {a : ℕ∞} (μ : Measure (Space d)) [μ.HasTemperateGrowth] : PolyBddSchwartzMap d a →L[] SpaceDHilbertSpace d μ := (schwartzIncl μ).domRestrict (PolyBddSchwartzMap d a), (schwartzIncl μ).continuous_domRestrict (schwartzIncl μ).continuous _

The submodule of SpaceDHilbertSpace d corresponding to bounded Schwartz maps.

abbrev PolyBddSchwartzSubmodule (d : ) (a : ℕ∞) (μ : Measure (Space d) := volume) [μ.HasTemperateGrowth] : Submodule (SpaceDHilbertSpace d μ) := (polyBddSchwartzIncl (a := a) μ).range
lemma polyBddSchwartzIncl_injective {d : } (a : ℕ∞) (μ : Measure (Space d)) [μ.HasTemperateGrowth] [μ.IsOpenPosMeasure] : Function.Injective (polyBddSchwartzIncl (a := a) μ) := LinearMap.injective_domRestrict_iff.mpr <| (schwartzIncl_ker μ).symm disjoint_bot_right

The linear equivalence between polynomially-bounded Schwartz maps and the corresponding submodule of the Hilbert space.

def polyBddSchwartzEquiv {d : } {a : ℕ∞} (μ : Measure (Space d)) [μ.HasTemperateGrowth] [μ.IsOpenPosMeasure] : PolyBddSchwartzMap d a ≃ₗ[] PolyBddSchwartzSubmodule d a μ := LinearEquiv.ofInjective (polyBddSchwartzIncl μ).toLinearMap (polyBddSchwartzIncl_injective a μ)

B. Coercions

instance : CoeOut (PolyBddSchwartzMap d a) 𝓢(Space d, ) := fun f f.valinstance : CoeFun (PolyBddSchwartzMap d a) (fun _ Space d ) := fun f f.val@[simp] lemma toFun_eq_coe (f : PolyBddSchwartzMap d a) (x : Space d) : f.val.toFun x = f.val x := rfld:a:ℕ∞μ:Measure (Space d)inst✝¹:μ.HasTemperateGrowthinst✝:μ.IsOpenPosMeasureψ:(SchwartzSubmodule d μ):ψ PolyBddSchwartzSubmodule d a μg:(PolyBddSchwartzMap d a)hg:(polyBddSchwartzEquiv μ) g = ψ, hg':(polyBddSchwartzIncl μ) g = ψ((schwartzEquiv μ) g) = (polyBddSchwartzIncl μ) g All goals completed! 🐙

C. (In)equalities

lemma PolyBddSchwartzMap_zero_eq_top (d : ) : PolyBddSchwartzMap d 0 = := d:PolyBddSchwartzMap d 0 = d:f:𝓢(Space d, )f PolyBddSchwartzMap d 0 f d:f:𝓢(Space d, )this: C, 0 < C (x : Space d), x ^ 0 * iteratedFDeriv 0 (⇑f) x Cf PolyBddSchwartzMap d 0 f All goals completed! 🐙lemma PolyBddSchwartzMap_antitone (d : ) {a b : ℕ∞} (h : a b) : PolyBddSchwartzMap d b PolyBddSchwartzMap d a := fun _ hx k hk hx k (hk.trans h)lemma of_zero_eq : PolyBddSchwartzSubmodule d 0 μ = SchwartzSubmodule d μ := d:μ:Measure (Space d)inst✝:μ.HasTemperateGrowthPolyBddSchwartzSubmodule d 0 μ = SchwartzSubmodule d μ All goals completed! 🐙lemma le_SchwartzSubmodule (d : ) (a : ℕ∞) : PolyBddSchwartzSubmodule d a SchwartzSubmodule d := LinearMap.range_domRestrict_le_range _ _lemma antitone {a b : ℕ∞} (h : a b) : PolyBddSchwartzSubmodule d b μ PolyBddSchwartzSubmodule d a μ := d:μ:Measure (Space d)inst✝:μ.HasTemperateGrowtha:ℕ∞b:ℕ∞h:a bPolyBddSchwartzSubmodule d b μ PolyBddSchwartzSubmodule d a μ d:μ:Measure (Space d)inst✝:μ.HasTemperateGrowtha:ℕ∞b:ℕ∞h:a bSubmodule.map (↑(schwartzIncl μ)) (PolyBddSchwartzMap d b) Submodule.map (↑(schwartzIncl μ)) (PolyBddSchwartzMap d a) All goals completed! 🐙

D. Density

𝕜:Type u_1E:Type u_2inst✝³:RCLike 𝕜inst✝²:NormedAddCommGroup Einst✝¹:NormedSpace Einst✝:HasContDiffBump Ec:Ef:ContDiffBump cg:E 𝕜x:E|f x| |1| All goals completed! 🐙μ:Measure (Space 0)inst✝¹:μ.HasTemperateGrowthinst✝:μ.IsOpenPosMeasurePolyBddSchwartzMap 0 = μ:Measure (Space 0)inst✝¹:μ.HasTemperateGrowthinst✝:μ.IsOpenPosMeasuref:𝓢(Space 0, )k:hk:k C, 0 < C (x : Space 0), x ^ (-k) * f x C refine 1 + f 0, μ:Measure (Space 0)inst✝¹:μ.HasTemperateGrowthinst✝:μ.IsOpenPosMeasuref:𝓢(Space 0, )k:hk:k 0 < 1 + f 0 All goals completed! 🐙, fun x ?_ μ:Measure (Space 0)inst✝¹:μ.HasTemperateGrowthinst✝:μ.IsOpenPosMeasuref:𝓢(Space 0, )k:hk:k x:Space 0(0 ^ k)⁻¹ * f 0 1 + f 0 μ:Measure (Space 0)inst✝¹:μ.HasTemperateGrowthinst✝:μ.IsOpenPosMeasuref:𝓢(Space 0, )x:Space 0hk:0 (0 ^ 0)⁻¹ * f 0 1 + f 0μ:Measure (Space 0)inst✝¹:μ.HasTemperateGrowthinst✝:μ.IsOpenPosMeasuref:𝓢(Space 0, )x:Space 0k:hk:(k + 1) (0 ^ (k + 1))⁻¹ * f 0 1 + f 0 μ:Measure (Space 0)inst✝¹:μ.HasTemperateGrowthinst✝:μ.IsOpenPosMeasuref:𝓢(Space 0, )x:Space 0hk:0 (0 ^ 0)⁻¹ * f 0 1 + f 0μ:Measure (Space 0)inst✝¹:μ.HasTemperateGrowthinst✝:μ.IsOpenPosMeasuref:𝓢(Space 0, )x:Space 0k:hk:(k + 1) (0 ^ (k + 1))⁻¹ * f 0 1 + f 0 All goals completed! 🐙TODO "Generalize density of PolyBddSchwartzSubmodule to more general measures than just μ ≤ volume."d:μ:Measure (Space d)inst✝²:μ.HasTemperateGrowth:μ volumeinst✝¹:μ.IsOpenPosMeasureinst✝:IsFiniteMeasureOnCompacts μhd:0 < dξ:(SpaceDHilbertSpace d μ)ψ: (SpaceDHilbertSpace d μ): (n : ), ψ n (SchwartzSubmodule d μ)hψξ:Tendsto ψ atTop (nhds ξ)f: 𝓢(Space d, ) := fun n => (schwartzEquiv μ).symm ψ n, b: ContDiffBump 0 := fun n => { rIn := (n + 1)⁻¹, rOut := 2 * (n + 1)⁻¹, rIn_pos := , rIn_lt_rOut := }g: 𝓢(Space d, ) := fun n => (smulLeftCLM (b n)) (f n)φ: (SpaceDHilbertSpace d μ) := fun n => (schwartzIncl μ) (g n)hg: (n : ) (x : Space d), (g n) x = ((b n) x) * (f n) xs: Space d := fun n x => ((b n) x) * ξ xσ: (SpaceDHilbertSpace d μ) := fun n => mk hψ_ae: (n : ), (ψ n) =ᵐ[μ] (f n)hφ_ae: (n : ), (φ n) =ᵐ[μ] (g n)hσ_ae: (n : ), (σ n) =ᵐ[μ] s nhφσ_ae: (n : ), ((φ - σ) n) =ᵐ[μ] (g n) - s nhψξ_ae: (n : ), (ψ n - ξ) =ᵐ[μ] (f n) - ξB: Set (Space d) := fun n => Metric.ball 0 (b n).rOuthξB:Tendsto (fun n => ∫⁻ (x : Space d) in B n, ξ x‖ₑ ^ 2 μ) atTop (nhds 0)n:h: (A : Set (Space d)), ∫⁻ (x : Space d) in A, (σ n) x‖ₑ ^ 2 μ = ∫⁻ (x : Space d) in A, s n x‖ₑ ^ 2 μ∫⁻ (x : Space d), s n x‖ₑ ^ 2 μ = ∫⁻ (x : Space d) in B n, s n x‖ₑ ^ 2 μ d:μ:Measure (Space d)inst✝²:μ.HasTemperateGrowth:μ volumeinst✝¹:μ.IsOpenPosMeasureinst✝:IsFiniteMeasureOnCompacts μhd:0 < dξ:(SpaceDHilbertSpace d μ)ψ: (SpaceDHilbertSpace d μ): (n : ), ψ n (SchwartzSubmodule d μ)hψξ:Tendsto ψ atTop (nhds ξ)f: 𝓢(Space d, ) := fun n => (schwartzEquiv μ).symm ψ n, b: ContDiffBump 0 := fun n => { rIn := (n + 1)⁻¹, rOut := 2 * (n + 1)⁻¹, rIn_pos := , rIn_lt_rOut := }g: 𝓢(Space d, ) := fun n => (smulLeftCLM (b n)) (f n)φ: (SpaceDHilbertSpace d μ) := fun n => (schwartzIncl μ) (g n)hg: (n : ) (x : Space d), (g n) x = ((b n) x) * (f n) xs: Space d := fun n x => ((b n) x) * ξ xσ: (SpaceDHilbertSpace d μ) := fun n => mk hψ_ae: (n : ), (ψ n) =ᵐ[μ] (f n)hφ_ae: (n : ), (φ n) =ᵐ[μ] (g n)hσ_ae: (n : ), (σ n) =ᵐ[μ] s nhφσ_ae: (n : ), ((φ - σ) n) =ᵐ[μ] (g n) - s nhψξ_ae: (n : ), (ψ n - ξ) =ᵐ[μ] (f n) - ξB: Set (Space d) := fun n => Metric.ball 0 (b n).rOuthξB:Tendsto (fun n => ∫⁻ (x : Space d) in B n, ξ x‖ₑ ^ 2 μ) atTop (nhds 0)n:h: (A : Set (Space d)), ∫⁻ (x : Space d) in A, (σ n) x‖ₑ ^ 2 μ = ∫⁻ (x : Space d) in A, s n x‖ₑ ^ 2 μ(Function.support fun x => s n x‖ₑ ^ 2) B n d:μ:Measure (Space d)inst✝²:μ.HasTemperateGrowth:μ volumeinst✝¹:μ.IsOpenPosMeasureinst✝:IsFiniteMeasureOnCompacts μhd:0 < dξ:(SpaceDHilbertSpace d μ)ψ: (SpaceDHilbertSpace d μ): (n : ), ψ n (SchwartzSubmodule d μ)hψξ:Tendsto ψ atTop (nhds ξ)f: 𝓢(Space d, ) := fun n => (schwartzEquiv μ).symm ψ n, b: ContDiffBump 0 := fun n => { rIn := (n + 1)⁻¹, rOut := 2 * (n + 1)⁻¹, rIn_pos := , rIn_lt_rOut := }g: 𝓢(Space d, ) := fun n => (smulLeftCLM (b n)) (f n)φ: (SpaceDHilbertSpace d μ) := fun n => (schwartzIncl μ) (g n)hg: (n : ) (x : Space d), (g n) x = ((b n) x) * (f n) xs: Space d := fun n x => ((b n) x) * ξ xσ: (SpaceDHilbertSpace d μ) := fun n => mk hψ_ae: (n : ), (ψ n) =ᵐ[μ] (f n)hφ_ae: (n : ), (φ n) =ᵐ[μ] (g n)hσ_ae: (n : ), (σ n) =ᵐ[μ] s nhφσ_ae: (n : ), ((φ - σ) n) =ᵐ[μ] (g n) - s nhψξ_ae: (n : ), (ψ n - ξ) =ᵐ[μ] (f n) - ξB: Set (Space d) := fun n => Metric.ball 0 (b n).rOuthξB:Tendsto (fun n => ∫⁻ (x : Space d) in B n, ξ x‖ₑ ^ 2 μ) atTop (nhds 0)n:h: (A : Set (Space d)), ∫⁻ (x : Space d) in A, (σ n) x‖ₑ ^ 2 μ = ∫⁻ (x : Space d) in A, s n x‖ₑ ^ 2 μx:Space dhx:x B ns n x‖ₑ ^ 2 = 0 All goals completed! 🐙 d:μ:Measure (Space d)inst✝²:μ.HasTemperateGrowth:μ volumeinst✝¹:μ.IsOpenPosMeasureinst✝:IsFiniteMeasureOnCompacts μhd:0 < dξ:(SpaceDHilbertSpace d μ)ψ: (SpaceDHilbertSpace d μ): (n : ), ψ n (SchwartzSubmodule d μ)hψξ:Tendsto ψ atTop (nhds ξ)f: 𝓢(Space d, ) := fun n => (schwartzEquiv μ).symm ψ n, b: ContDiffBump 0 := fun n => { rIn := (n + 1)⁻¹, rOut := 2 * (n + 1)⁻¹, rIn_pos := , rIn_lt_rOut := }g: 𝓢(Space d, ) := fun n => (smulLeftCLM (b n)) (f n)φ: (SpaceDHilbertSpace d μ) := fun n => (schwartzIncl μ) (g n)hg: (n : ) (x : Space d), (g n) x = ((b n) x) * (f n) xs: Space d := fun n x => ((b n) x) * ξ xσ: (SpaceDHilbertSpace d μ) := fun n => mk hψ_ae: (n : ), (ψ n) =ᵐ[μ] (f n)hφ_ae: (n : ), (φ n) =ᵐ[μ] (g n)hσ_ae: (n : ), (σ n) =ᵐ[μ] s nhφσ_ae: (n : ), ((φ - σ) n) =ᵐ[μ] (g n) - s nhψξ_ae: (n : ), (ψ n - ξ) =ᵐ[μ] (f n) - ξTendsto (φ - σ) atTop (nhds 0) -- `φₙ - σₙ = bₙ(ψₙ - ξ) → 0` since `ψₙ → ξ` (by definition) and the `bₙ` are bounded d:μ:Measure (Space d)inst✝²:μ.HasTemperateGrowth:μ volumeinst✝¹:μ.IsOpenPosMeasureinst✝:IsFiniteMeasureOnCompacts μhd:0 < dξ:(SpaceDHilbertSpace d μ)ψ: (SpaceDHilbertSpace d μ): (n : ), ψ n (SchwartzSubmodule d μ)hψξ:Tendsto ψ atTop (nhds ξ)f: 𝓢(Space d, ) := fun n => (schwartzEquiv μ).symm ψ n, b: ContDiffBump 0 := fun n => { rIn := (n + 1)⁻¹, rOut := 2 * (n + 1)⁻¹, rIn_pos := , rIn_lt_rOut := }g: 𝓢(Space d, ) := fun n => (smulLeftCLM (b n)) (f n)φ: (SpaceDHilbertSpace d μ) := fun n => (schwartzIncl μ) (g n)hg: (n : ) (x : Space d), (g n) x = ((b n) x) * (f n) xs: Space d := fun n x => ((b n) x) * ξ xσ: (SpaceDHilbertSpace d μ) := fun n => mk hψ_ae: (n : ), (ψ n) =ᵐ[μ] (f n)hφ_ae: (n : ), (φ n) =ᵐ[μ] (g n)hσ_ae: (n : ), (σ n) =ᵐ[μ] s nhφσ_ae: (n : ), ((φ - σ) n) =ᵐ[μ] (g n) - s nhψξ_ae: (n : ), (ψ n - ξ) =ᵐ[μ] (f n) - ξTendsto (fun a => ∫⁻ (x : Space d), ((φ - σ) a) x‖ₑ ^ 2 μ) atTop (nhds 0) d:μ:Measure (Space d)inst✝²:μ.HasTemperateGrowth:μ volumeinst✝¹:μ.IsOpenPosMeasureinst✝:IsFiniteMeasureOnCompacts μhd:0 < dξ:(SpaceDHilbertSpace d μ)ψ: (SpaceDHilbertSpace d μ): (n : ), ψ n (SchwartzSubmodule d μ)hψξ✝:Tendsto ψ atTop (nhds ξ)f: 𝓢(Space d, ) := fun n => (schwartzEquiv μ).symm ψ n, b: ContDiffBump 0 := fun n => { rIn := (n + 1)⁻¹, rOut := 2 * (n + 1)⁻¹, rIn_pos := , rIn_lt_rOut := }g: 𝓢(Space d, ) := fun n => (smulLeftCLM (b n)) (f n)φ: (SpaceDHilbertSpace d μ) := fun n => (schwartzIncl μ) (g n)hg: (n : ) (x : Space d), (g n) x = ((b n) x) * (f n) xs: Space d := fun n x => ((b n) x) * ξ xσ: (SpaceDHilbertSpace d μ) := fun n => mk hψ_ae: (n : ), (ψ n) =ᵐ[μ] (f n)hφ_ae: (n : ), (φ n) =ᵐ[μ] (g n)hσ_ae: (n : ), (σ n) =ᵐ[μ] s nhφσ_ae: (n : ), ((φ - σ) n) =ᵐ[μ] (g n) - s nhψξ_ae: (n : ), (ψ n - ξ) =ᵐ[μ] (f n) - ξhψξ:Tendsto (fun n => ∫⁻ (x : Space d), (ψ n - ξ) x‖ₑ ^ 2 μ) atTop (nhds 0)Tendsto (fun a => ∫⁻ (x : Space d), ((φ - σ) a) x‖ₑ ^ 2 μ) atTop (nhds 0) d:μ:Measure (Space d)inst✝²:μ.HasTemperateGrowth:μ volumeinst✝¹:μ.IsOpenPosMeasureinst✝:IsFiniteMeasureOnCompacts μhd:0 < dξ:(SpaceDHilbertSpace d μ)ψ: (SpaceDHilbertSpace d μ): (n : ), ψ n (SchwartzSubmodule d μ)hψξ✝:Tendsto ψ atTop (nhds ξ)f: 𝓢(Space d, ) := fun n => (schwartzEquiv μ).symm ψ n, b: ContDiffBump 0 := fun n => { rIn := (n + 1)⁻¹, rOut := 2 * (n + 1)⁻¹, rIn_pos := , rIn_lt_rOut := }g: 𝓢(Space d, ) := fun n => (smulLeftCLM (b n)) (f n)φ: (SpaceDHilbertSpace d μ) := fun n => (schwartzIncl μ) (g n)hg: (n : ) (x : Space d), (g n) x = ((b n) x) * (f n) xs: Space d := fun n x => ((b n) x) * ξ xσ: (SpaceDHilbertSpace d μ) := fun n => mk hψ_ae: (n : ), (ψ n) =ᵐ[μ] (f n)hφ_ae: (n : ), (φ n) =ᵐ[μ] (g n)hσ_ae: (n : ), (σ n) =ᵐ[μ] s nhφσ_ae: (n : ), ((φ - σ) n) =ᵐ[μ] (g n) - s nhψξ_ae: (n : ), (ψ n - ξ) =ᵐ[μ] (f n) - ξhψξ:Tendsto (fun n => ∫⁻ (x : Space d), (ψ n - ξ) x‖ₑ ^ 2 μ) atTop (nhds 0)n:∫⁻ (x : Space d), ((φ - σ) n) x‖ₑ ^ 2 μ ∫⁻ (x : Space d), (ψ n - ξ) x‖ₑ ^ 2 μ d:μ:Measure (Space d)inst✝²:μ.HasTemperateGrowth:μ volumeinst✝¹:μ.IsOpenPosMeasureinst✝:IsFiniteMeasureOnCompacts μhd:0 < dξ:(SpaceDHilbertSpace d μ)ψ: (SpaceDHilbertSpace d μ): (n : ), ψ n (SchwartzSubmodule d μ)hψξ✝:Tendsto ψ atTop (nhds ξ)f: 𝓢(Space d, ) := fun n => (schwartzEquiv μ).symm ψ n, b: ContDiffBump 0 := fun n => { rIn := (n + 1)⁻¹, rOut := 2 * (n + 1)⁻¹, rIn_pos := , rIn_lt_rOut := }g: 𝓢(Space d, ) := fun n => (smulLeftCLM (b n)) (f n)φ: (SpaceDHilbertSpace d μ) := fun n => (schwartzIncl μ) (g n)hg: (n : ) (x : Space d), (g n) x = ((b n) x) * (f n) xs: Space d := fun n x => ((b n) x) * ξ xσ: (SpaceDHilbertSpace d μ) := fun n => mk hψ_ae: (n : ), (ψ n) =ᵐ[μ] (f n)hφ_ae: (n : ), (φ n) =ᵐ[μ] (g n)hσ_ae: (n : ), (σ n) =ᵐ[μ] s nhφσ_ae: (n : ), ((φ - σ) n) =ᵐ[μ] (g n) - s nhψξ_ae: (n : ), (ψ n - ξ) =ᵐ[μ] (f n) - ξhψξ:Tendsto (fun n => ∫⁻ (x : Space d), (ψ n - ξ) x‖ₑ ^ 2 μ) atTop (nhds 0)n:∀ᵐ (a : Space d) μ, ((φ - σ) n) a‖ₑ ^ 2 (ψ n - ξ) a‖ₑ ^ 2 filter_upwards [hφσ_ae n, hψξ_ae n] with x d:μ:Measure (Space d)inst✝²:μ.HasTemperateGrowth:μ volumeinst✝¹:μ.IsOpenPosMeasureinst✝:IsFiniteMeasureOnCompacts μhd:0 < dξ:(SpaceDHilbertSpace d μ)ψ: (SpaceDHilbertSpace d μ): (n : ), ψ n (SchwartzSubmodule d μ)hψξ✝:Tendsto ψ atTop (nhds ξ)f: 𝓢(Space d, ) := fun n => (schwartzEquiv μ).symm ψ n, b: ContDiffBump 0 := fun n => { rIn := (n + 1)⁻¹, rOut := 2 * (n + 1)⁻¹, rIn_pos := , rIn_lt_rOut := }g: 𝓢(Space d, ) := fun n => (smulLeftCLM (b n)) (f n)φ: (SpaceDHilbertSpace d μ) := fun n => (schwartzIncl μ) (g n)hg: (n : ) (x : Space d), (g n) x = ((b n) x) * (f n) xs: Space d := fun n x => ((b n) x) * ξ xσ: (SpaceDHilbertSpace d μ) := fun n => mk hψ_ae: (n : ), (ψ n) =ᵐ[μ] (f n)hφ_ae: (n : ), (φ n) =ᵐ[μ] (g n)hσ_ae: (n : ), (σ n) =ᵐ[μ] s nhφσ_ae: (n : ), ((φ - σ) n) =ᵐ[μ] (g n) - s nhψξ_ae: (n : ), (ψ n - ξ) =ᵐ[μ] (f n) - ξhψξ:Tendsto (fun n => ∫⁻ (x : Space d), (ψ n - ξ) x‖ₑ ^ 2 μ) atTop (nhds 0)n:x:Space dh:((φ - σ) n) x = ((g n) - s n) x(ψ n - ξ) x = ((f n) - ξ) x ((φ - σ) n) x‖ₑ ^ 2 (ψ n - ξ) x‖ₑ ^ 2 d:μ:Measure (Space d)inst✝²:μ.HasTemperateGrowth:μ volumeinst✝¹:μ.IsOpenPosMeasureinst✝:IsFiniteMeasureOnCompacts μhd:0 < dξ:(SpaceDHilbertSpace d μ)ψ: (SpaceDHilbertSpace d μ): (n : ), ψ n (SchwartzSubmodule d μ)hψξ✝:Tendsto ψ atTop (nhds ξ)f: 𝓢(Space d, ) := fun n => (schwartzEquiv μ).symm ψ n, b: ContDiffBump 0 := fun n => { rIn := (n + 1)⁻¹, rOut := 2 * (n + 1)⁻¹, rIn_pos := , rIn_lt_rOut := }g: 𝓢(Space d, ) := fun n => (smulLeftCLM (b n)) (f n)φ: (SpaceDHilbertSpace d μ) := fun n => (schwartzIncl μ) (g n)hg: (n : ) (x : Space d), (g n) x = ((b n) x) * (f n) xs: Space d := fun n x => ((b n) x) * ξ xσ: (SpaceDHilbertSpace d μ) := fun n => mk hψ_ae: (n : ), (ψ n) =ᵐ[μ] (f n)hφ_ae: (n : ), (φ n) =ᵐ[μ] (g n)hσ_ae: (n : ), (σ n) =ᵐ[μ] s nhφσ_ae: (n : ), ((φ - σ) n) =ᵐ[μ] (g n) - s nhψξ_ae: (n : ), (ψ n - ξ) =ᵐ[μ] (f n) - ξhψξ:Tendsto (fun n => ∫⁻ (x : Space d), (ψ n - ξ) x‖ₑ ^ 2 μ) atTop (nhds 0)n:x:Space dh:((φ - σ) n) x = ((g n) - s n) xh':(ψ n - ξ) x = ((f n) - ξ) x((φ - σ) n) x‖ₑ ^ 2 (ψ n - ξ) x‖ₑ ^ 2 simp_rw d:μ:Measure (Space d)inst✝²:μ.HasTemperateGrowth:μ volumeinst✝¹:μ.IsOpenPosMeasureinst✝:IsFiniteMeasureOnCompacts μhd:0 < dξ:(SpaceDHilbertSpace d μ)ψ: (SpaceDHilbertSpace d μ): (n : ), ψ n (SchwartzSubmodule d μ)hψξ✝:Tendsto ψ atTop (nhds ξ)f: 𝓢(Space d, ) := fun n => (schwartzEquiv μ).symm ψ n, b: ContDiffBump 0 := fun n => { rIn := (n + 1)⁻¹, rOut := 2 * (n + 1)⁻¹, rIn_pos := , rIn_lt_rOut := }g: 𝓢(Space d, ) := fun n => (smulLeftCLM (b n)) (f n)φ: (SpaceDHilbertSpace d μ) := fun n => (schwartzIncl μ) (g n)hg: (n : ) (x : Space d), (g n) x = ((b n) x) * (f n) xs: Space d := fun n x => ((b n) x) * ξ xσ: (SpaceDHilbertSpace d μ) := fun n => mk hψ_ae: (n : ), (ψ n) =ᵐ[μ] (f n)hφ_ae: (n : ), (φ n) =ᵐ[μ] (g n)hσ_ae: (n : ), (σ n) =ᵐ[μ] s nhφσ_ae: (n : ), ((φ - σ) n) =ᵐ[μ] (g n) - s nhψξ_ae: (n : ), (ψ n - ξ) =ᵐ[μ] (f n) - ξhψξ:Tendsto (fun n => ∫⁻ (x : Space d), (ψ n - ξ) x‖ₑ ^ 2 μ) atTop (nhds 0)n:x:Space dh:((φ - σ) n) x = ((g n) - s n) xh':(ψ n - ξ) x = ((f n) - ξ) x((φ - σ) n) x‖ₑ ^ 2 (ψ n - ξ) x‖ₑ ^ 2d:μ:Measure (Space d)inst✝²:μ.HasTemperateGrowth:μ volumeinst✝¹:μ.IsOpenPosMeasureinst✝:IsFiniteMeasureOnCompacts μhd:0 < dξ:(SpaceDHilbertSpace d μ)ψ: (SpaceDHilbertSpace d μ): (n : ), ψ n (SchwartzSubmodule d μ)hψξ✝:Tendsto ψ atTop (nhds ξ)f: 𝓢(Space d, ) := fun n => (schwartzEquiv μ).symm ψ n, b: ContDiffBump 0 := fun n => { rIn := (n + 1)⁻¹, rOut := 2 * (n + 1)⁻¹, rIn_pos := , rIn_lt_rOut := }g: 𝓢(Space d, ) := fun n => (smulLeftCLM (b n)) (f n)φ: (SpaceDHilbertSpace d μ) := fun n => (schwartzIncl μ) (g n)hg: (n : ) (x : Space d), (g n) x = ((b n) x) * (f n) xs: Space d := fun n x => ((b n) x) * ξ xσ: (SpaceDHilbertSpace d μ) := fun n => mk hψ_ae: (n : ), (ψ n) =ᵐ[μ] (f n)hφ_ae: (n : ), (φ n) =ᵐ[μ] (g n)hσ_ae: (n : ), (σ n) =ᵐ[μ] s nhφσ_ae: (n : ), ((φ - σ) n) =ᵐ[μ] (g n) - s nhψξ_ae: (n : ), (ψ n - ξ) =ᵐ[μ] (f n) - ξhψξ:Tendsto (fun n => ∫⁻ (x : Space d), (ψ n - ξ) x‖ₑ ^ 2 μ) atTop (nhds 0)n:x:Space dh:((φ - σ) n) x = ((g n) - s n) xh':(ψ n - ξ) x = ((f n) - ξ) x((g n) - s n) x‖ₑ ^ 2 (ψ n - ξ) x‖ₑ ^ 2 d:μ:Measure (Space d)inst✝²:μ.HasTemperateGrowth:μ volumeinst✝¹:μ.IsOpenPosMeasureinst✝:IsFiniteMeasureOnCompacts μhd:0 < dξ:(SpaceDHilbertSpace d μ)ψ: (SpaceDHilbertSpace d μ): (n : ), ψ n (SchwartzSubmodule d μ)hψξ✝:Tendsto ψ atTop (nhds ξ)f: 𝓢(Space d, ) := fun n => (schwartzEquiv μ).symm ψ n, b: ContDiffBump 0 := fun n => { rIn := (n + 1)⁻¹, rOut := 2 * (n + 1)⁻¹, rIn_pos := , rIn_lt_rOut := }g: 𝓢(Space d, ) := fun n => (smulLeftCLM (b n)) (f n)φ: (SpaceDHilbertSpace d μ) := fun n => (schwartzIncl μ) (g n)hg: (n : ) (x : Space d), (g n) x = ((b n) x) * (f n) xs: Space d := fun n x => ((b n) x) * ξ xσ: (SpaceDHilbertSpace d μ) := fun n => mk hψ_ae: (n : ), (ψ n) =ᵐ[μ] (f n)hφ_ae: (n : ), (φ n) =ᵐ[μ] (g n)hσ_ae: (n : ), (σ n) =ᵐ[μ] s nhφσ_ae: (n : ), ((φ - σ) n) =ᵐ[μ] (g n) - s nhψξ_ae: (n : ), (ψ n - ξ) =ᵐ[μ] (f n) - ξhψξ:Tendsto (fun n => ∫⁻ (x : Space d), (ψ n - ξ) x‖ₑ ^ 2 μ) atTop (nhds 0)n:x:Space dh:((φ - σ) n) x = ((g n) - s n) xh':(ψ n - ξ) x = ((f n) - ξ) x((g n) - s n) x‖ₑ ^ 2 ((f n) - ξ) x‖ₑ ^ 2 d:μ:Measure (Space d)inst✝²:μ.HasTemperateGrowth:μ volumeinst✝¹:μ.IsOpenPosMeasureinst✝:IsFiniteMeasureOnCompacts μhd:0 < dξ:(SpaceDHilbertSpace d μ)ψ: (SpaceDHilbertSpace d μ): (n : ), ψ n (SchwartzSubmodule d μ)hψξ✝:Tendsto ψ atTop (nhds ξ)f: 𝓢(Space d, ) := fun n => (schwartzEquiv μ).symm ψ n, b: ContDiffBump 0 := fun n => { rIn := (n + 1)⁻¹, rOut := 2 * (n + 1)⁻¹, rIn_pos := , rIn_lt_rOut := }g: 𝓢(Space d, ) := fun n => (smulLeftCLM (b n)) (f n)φ: (SpaceDHilbertSpace d μ) := fun n => (schwartzIncl μ) (g n)hg: (n : ) (x : Space d), (g n) x = ((b n) x) * (f n) xs: Space d := fun n x => ((b n) x) * ξ xσ: (SpaceDHilbertSpace d μ) := fun n => mk hψ_ae: (n : ), (ψ n) =ᵐ[μ] (f n)hφ_ae: (n : ), (φ n) =ᵐ[μ] (g n)hσ_ae: (n : ), (σ n) =ᵐ[μ] s nhφσ_ae: (n : ), ((φ - σ) n) =ᵐ[μ] (g n) - s nhψξ_ae: (n : ), (ψ n - ξ) =ᵐ[μ] (f n) - ξhψξ:Tendsto (fun n => ∫⁻ (x : Space d), (ψ n - ξ) x‖ₑ ^ 2 μ) atTop (nhds 0)n:x:Space dh:((φ - σ) n) x = ((g n) - s n) xh':(ψ n - ξ) x = ((f n) - ξ) x(g n) x - s n x‖ₑ ^ 2 (f n) x - ξ x‖ₑ ^ 2 d:μ:Measure (Space d)inst✝²:μ.HasTemperateGrowth:μ volumeinst✝¹:μ.IsOpenPosMeasureinst✝:IsFiniteMeasureOnCompacts μhd:0 < dξ:(SpaceDHilbertSpace d μ)ψ: (SpaceDHilbertSpace d μ): (n : ), ψ n (SchwartzSubmodule d μ)hψξ✝:Tendsto ψ atTop (nhds ξ)f: 𝓢(Space d, ) := fun n => (schwartzEquiv μ).symm ψ n, b: ContDiffBump 0 := fun n => { rIn := (n + 1)⁻¹, rOut := 2 * (n + 1)⁻¹, rIn_pos := , rIn_lt_rOut := }g: 𝓢(Space d, ) := fun n => (smulLeftCLM (b n)) (f n)φ: (SpaceDHilbertSpace d μ) := fun n => (schwartzIncl μ) (g n)hg: (n : ) (x : Space d), (g n) x = ((b n) x) * (f n) xs: Space d := fun n x => ((b n) x) * ξ xσ: (SpaceDHilbertSpace d μ) := fun n => mk hψ_ae: (n : ), (ψ n) =ᵐ[μ] (f n)hφ_ae: (n : ), (φ n) =ᵐ[μ] (g n)hσ_ae: (n : ), (σ n) =ᵐ[μ] s nhφσ_ae: (n : ), ((φ - σ) n) =ᵐ[μ] (g n) - s nhψξ_ae: (n : ), (ψ n - ξ) =ᵐ[μ] (f n) - ξhψξ:Tendsto (fun n => ∫⁻ (x : Space d), (ψ n - ξ) x‖ₑ ^ 2 μ) atTop (nhds 0)n:x:Space dh:((φ - σ) n) x = ((g n) - s n) xh':(ψ n - ξ) x = ((f n) - ξ) x((b n) x) * (f n) x - s n x‖ₑ ^ 2 (f n) x - ξ x‖ₑ ^ 2 d:μ:Measure (Space d)inst✝²:μ.HasTemperateGrowth:μ volumeinst✝¹:μ.IsOpenPosMeasureinst✝:IsFiniteMeasureOnCompacts μhd:0 < dξ:(SpaceDHilbertSpace d μ)ψ: (SpaceDHilbertSpace d μ): (n : ), ψ n (SchwartzSubmodule d μ)hψξ✝:Tendsto ψ atTop (nhds ξ)f: 𝓢(Space d, ) := fun n => (schwartzEquiv μ).symm ψ n, b: ContDiffBump 0 := fun n => { rIn := (n + 1)⁻¹, rOut := 2 * (n + 1)⁻¹, rIn_pos := , rIn_lt_rOut := }g: 𝓢(Space d, ) := fun n => (smulLeftCLM (b n)) (f n)φ: (SpaceDHilbertSpace d μ) := fun n => (schwartzIncl μ) (g n)hg: (n : ) (x : Space d), (g n) x = ((b n) x) * (f n) xs: Space d := fun n x => ((b n) x) * ξ xσ: (SpaceDHilbertSpace d μ) := fun n => mk hψ_ae: (n : ), (ψ n) =ᵐ[μ] (f n)hφ_ae: (n : ), (φ n) =ᵐ[μ] (g n)hσ_ae: (n : ), (σ n) =ᵐ[μ] s nhφσ_ae: (n : ), ((φ - σ) n) =ᵐ[μ] (g n) - s nhψξ_ae: (n : ), (ψ n - ξ) =ᵐ[μ] (f n) - ξhψξ:Tendsto (fun n => ∫⁻ (x : Space d), (ψ n - ξ) x‖ₑ ^ 2 μ) atTop (nhds 0)n:x:Space dh:((φ - σ) n) x = ((g n) - s n) xh':(ψ n - ξ) x = ((f n) - ξ) x((b n) x) * (f n) x - ((b n) x) * ξ x‖ₑ ^ 2 (f n) x - ξ x‖ₑ ^ 2 d:μ:Measure (Space d)inst✝²:μ.HasTemperateGrowth:μ volumeinst✝¹:μ.IsOpenPosMeasureinst✝:IsFiniteMeasureOnCompacts μhd:0 < dξ:(SpaceDHilbertSpace d μ)ψ: (SpaceDHilbertSpace d μ): (n : ), ψ n (SchwartzSubmodule d μ)hψξ✝:Tendsto ψ atTop (nhds ξ)f: 𝓢(Space d, ) := fun n => (schwartzEquiv μ).symm ψ n, b: ContDiffBump 0 := fun n => { rIn := (n + 1)⁻¹, rOut := 2 * (n + 1)⁻¹, rIn_pos := , rIn_lt_rOut := }g: 𝓢(Space d, ) := fun n => (smulLeftCLM (b n)) (f n)φ: (SpaceDHilbertSpace d μ) := fun n => (schwartzIncl μ) (g n)hg: (n : ) (x : Space d), (g n) x = ((b n) x) * (f n) xs: Space d := fun n x => ((b n) x) * ξ xσ: (SpaceDHilbertSpace d μ) := fun n => mk hψ_ae: (n : ), (ψ n) =ᵐ[μ] (f n)hφ_ae: (n : ), (φ n) =ᵐ[μ] (g n)hσ_ae: (n : ), (σ n) =ᵐ[μ] s nhφσ_ae: (n : ), ((φ - σ) n) =ᵐ[μ] (g n) - s nhψξ_ae: (n : ), (ψ n - ξ) =ᵐ[μ] (f n) - ξhψξ:Tendsto (fun n => ∫⁻ (x : Space d), (ψ n - ξ) x‖ₑ ^ 2 μ) atTop (nhds 0)n:x:Space dh:((φ - σ) n) x = ((g n) - s n) xh':(ψ n - ξ) x = ((f n) - ξ) x((b n) x) * ((f n) x - ξ x)‖ₑ ^ 2 (f n) x - ξ x‖ₑ ^ 2] All goals completed! 🐙lemma dense ( : μ volume) [μ.IsOpenPosMeasure] [IsFiniteMeasureOnCompacts μ] : Dense (PolyBddSchwartzSubmodule d a μ : Set (SpaceDHilbertSpace d μ)) := (dense_top μ ).mono (antitone μ le_top)