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 d⊢ ‖c‖ * (‖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 d⊢ ‖c‖ * 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.val⟩instance : 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 μ)hψ:↑ψ ∈ PolyBddSchwartzSubmodule d a μg:↥(PolyBddSchwartzMap d a)hg:(polyBddSchwartzEquiv μ) g = ⟨↑ψ, hψ⟩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‖ ≤ C⊢ f ∈ 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✝:μ.HasTemperateGrowth⊢ PolyBddSchwartzSubmodule 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 ≤ b⊢ PolyBddSchwartzSubmodule d b μ ≤ PolyBddSchwartzSubmodule d a μ d:ℕμ:Measure (Space d)inst✝:μ.HasTemperateGrowtha:ℕ∞b:ℕ∞h:a ≤ b⊢ Submodule.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✝:μ.IsOpenPosMeasure⊢ PolyBddSchwartzMap 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✝²:μ.HasTemperateGrowthhμ:μ ≤ volumeinst✝¹:μ.IsOpenPosMeasureinst✝:IsFiniteMeasureOnCompacts μhd:0 < dξ:↥(SpaceDHilbertSpace d μ)ψ:ℕ → ↥(SpaceDHilbertSpace d μ)hψ:∀ (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✝²:μ.HasTemperateGrowthhμ:μ ≤ volumeinst✝¹:μ.IsOpenPosMeasureinst✝:IsFiniteMeasureOnCompacts μhd:0 < dξ:↥(SpaceDHilbertSpace d μ)ψ:ℕ → ↥(SpaceDHilbertSpace d μ)hψ:∀ (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✝²:μ.HasTemperateGrowthhμ:μ ≤ volumeinst✝¹:μ.IsOpenPosMeasureinst✝:IsFiniteMeasureOnCompacts μhd:0 < dξ:↥(SpaceDHilbertSpace d μ)ψ:ℕ → ↥(SpaceDHilbertSpace d μ)hψ:∀ (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 n⊢ ‖s n x‖ₑ ^ 2 = 0 All goals completed! 🐙 d:ℕμ:Measure (Space d)inst✝²:μ.HasTemperateGrowthhμ:μ ≤ volumeinst✝¹:μ.IsOpenPosMeasureinst✝:IsFiniteMeasureOnCompacts μhd:0 < dξ:↥(SpaceDHilbertSpace d μ)ψ:ℕ → ↥(SpaceDHilbertSpace d μ)hψ:∀ (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✝²:μ.HasTemperateGrowthhμ:μ ≤ volumeinst✝¹:μ.IsOpenPosMeasureinst✝:IsFiniteMeasureOnCompacts μhd:0 < dξ:↥(SpaceDHilbertSpace d μ)ψ:ℕ → ↥(SpaceDHilbertSpace d μ)hψ:∀ (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✝²:μ.HasTemperateGrowthhμ:μ ≤ volumeinst✝¹:μ.IsOpenPosMeasureinst✝:IsFiniteMeasureOnCompacts μhd:0 < dξ:↥(SpaceDHilbertSpace d μ)ψ:ℕ → ↥(SpaceDHilbertSpace d μ)hψ:∀ (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✝²:μ.HasTemperateGrowthhμ:μ ≤ volumeinst✝¹:μ.IsOpenPosMeasureinst✝:IsFiniteMeasureOnCompacts μhd:0 < dξ:↥(SpaceDHilbertSpace d μ)ψ:ℕ → ↥(SpaceDHilbertSpace d μ)hψ:∀ (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✝²:μ.HasTemperateGrowthhμ:μ ≤ volumeinst✝¹:μ.IsOpenPosMeasureinst✝:IsFiniteMeasureOnCompacts μhd:0 < dξ:↥(SpaceDHilbertSpace d μ)ψ:ℕ → ↥(SpaceDHilbertSpace d μ)hψ:∀ (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✝²:μ.HasTemperateGrowthhμ:μ ≤ volumeinst✝¹:μ.IsOpenPosMeasureinst✝:IsFiniteMeasureOnCompacts μhd:0 < dξ:↥(SpaceDHilbertSpace d μ)ψ:ℕ → ↥(SpaceDHilbertSpace d μ)hψ:∀ (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✝²:μ.HasTemperateGrowthhμ:μ ≤ volumeinst✝¹:μ.IsOpenPosMeasureinst✝:IsFiniteMeasureOnCompacts μhd:0 < dξ:↥(SpaceDHilbertSpace d μ)ψ:ℕ → ↥(SpaceDHilbertSpace d μ)hψ:∀ (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✝²:μ.HasTemperateGrowthhμ:μ ≤ volumeinst✝¹:μ.IsOpenPosMeasureinst✝:IsFiniteMeasureOnCompacts μhd:0 < dξ:↥(SpaceDHilbertSpace d μ)ψ:ℕ → ↥(SpaceDHilbertSpace d μ)hψ:∀ (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✝²:μ.HasTemperateGrowthhμ:μ ≤ volumeinst✝¹:μ.IsOpenPosMeasureinst✝:IsFiniteMeasureOnCompacts μhd:0 < dξ:↥(SpaceDHilbertSpace d μ)ψ:ℕ → ↥(SpaceDHilbertSpace d μ)hψ:∀ (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✝²:μ.HasTemperateGrowthhμ:μ ≤ volumeinst✝¹:μ.IsOpenPosMeasureinst✝:IsFiniteMeasureOnCompacts μhd:0 < dξ:↥(SpaceDHilbertSpace d μ)ψ:ℕ → ↥(SpaceDHilbertSpace d μ)hψ:∀ (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✝²:μ.HasTemperateGrowthhμ:μ ≤ volumeinst✝¹:μ.IsOpenPosMeasureinst✝:IsFiniteMeasureOnCompacts μhd:0 < dξ:↥(SpaceDHilbertSpace d μ)ψ:ℕ → ↥(SpaceDHilbertSpace d μ)hψ:∀ (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✝²:μ.HasTemperateGrowthhμ:μ ≤ volumeinst✝¹:μ.IsOpenPosMeasureinst✝:IsFiniteMeasureOnCompacts μhd:0 < dξ:↥(SpaceDHilbertSpace d μ)ψ:ℕ → ↥(SpaceDHilbertSpace d μ)hψ:∀ (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✝²:μ.HasTemperateGrowthhμ:μ ≤ volumeinst✝¹:μ.IsOpenPosMeasureinst✝:IsFiniteMeasureOnCompacts μhd:0 < dξ:↥(SpaceDHilbertSpace d μ)ψ:ℕ → ↥(SpaceDHilbertSpace d μ)hψ:∀ (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✝²:μ.HasTemperateGrowthhμ:μ ≤ volumeinst✝¹:μ.IsOpenPosMeasureinst✝:IsFiniteMeasureOnCompacts μhd:0 < dξ:↥(SpaceDHilbertSpace d μ)ψ:ℕ → ↥(SpaceDHilbertSpace d μ)hψ:∀ (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 (hμ : μ ≤ volume) [μ.IsOpenPosMeasure] [IsFiniteMeasureOnCompacts μ] : Dense (PolyBddSchwartzSubmodule d a μ : Set (SpaceDHilbertSpace d μ)) := (dense_top μ hμ).mono (antitone μ le_top)