Physlib.QuantumMechanics.HilbertSpaces.SpaceD.SchwartzSubmodule

Imports

/-
Copyright (c) 2026 Gregory J. Loges. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Adam Bornemann, Gregory J. Loges
-/
module

public import Mathlib.Analysis.Distribution.SchwartzSpace.Basic
public import Physlib.QuantumMechanics.HilbertSpaces.SpaceD.Basic

Schwartz submodule

i. Overview

In this module we define the Schwartz submodule of SpaceDHilbertSpace d μ. SchwartzSubmodule d μ consists of the μ-a.e. equal equivalence classes of Schwartz maps on Space d.

This is an import subspace of the Hilbert space. For one, the Fourier transform maps the Schwartz submodule into itself. It also is a convenient dense domain on which to define derivative operators.

ii. Key results

SchwartzSubmodule d μ: Submodule of SpaceDHilbertSpace d μ consisting of the L² equivalence classes of Schwartz maps 𝓢(Space d, ℂ).

SchwartzSubmoduleOn Ω μ: The projection of SchwartzSubmodule d μ onto SpaceDHilbertSpaceOn Ω μ.

iii. Table of contents

A. SchwartzSubmodule

A.1. Coercions

A.2. Misc.

B. SchwartzSubmoduleOn

iv. References

@[expose] public section

A. SchwartzSubmodule

The continuous linear map including Schwartz maps into SpaceDHilbertSpace d μ.

def schwartzIncl {d : ℕ} (μ : Measure (Space d)) [μ.HasTemperateGrowth] :
    𝓢(Space d, ℂ) →L[ℂ] SpaceDHilbertSpace d μ :=
  toLpCLM ℂ ℂ 2 μ

The submodule of SpaceDHilbertSpace d corresponding to Schwartz maps.

abbrev SchwartzSubmodule (d : ℕ) (μ : Measure (Space d) := volume) [μ.HasTemperateGrowth] :
    Submodule ℂ (SpaceDHilbertSpace d μ) :=
  (schwartzIncl μ).range

The linear equivalence between the Schwartz maps 𝓢(Space d, ℂ) and the Schwartz submodule of SpaceDHilbertSpace d μ.

def schwartzEquiv
    {d : ℕ} (μ : Measure (Space d)) [μ.HasTemperateGrowth] [μ.IsOpenPosMeasure] :
    𝓢(Space d, ℂ) ≃ₗ[ℂ] SchwartzSubmodule d μ :=
  LinearEquiv.ofInjective (schwartzIncl μ).toLinearMap (injective_toLp 2 μ)

A.1. Coercions

              instance : CoeFun (SchwartzSubmodule d μ) fun _ ↦ Space d → ℂ := ⟨fun ψ ↦ ψ.val⟩lemma schwartzEquiv_apply_coe : ↑(schwartzEquiv μ f) = schwartzIncl μ f := byd:ℕμ:Measure (Space d)inst✝¹:μ.HasTemperateGrowthinst✝:μ.IsOpenPosMeasuref:𝓢(Space d, ℂ)⊢ ↑((schwartzEquiv μ) f) = (schwartzIncl μ) f simp [schwartzEquiv]All goals completed! 🐙lemma schwartzEquiv_coe_ae : schwartzEquiv μ f =ᵐ[μ] f := coeFn_toLp f 2 μlemma schwartzEquiv_symm_coe_ae : (schwartzEquiv μ).symm ψ =ᵐ[μ] ψ := byd:ℕμ:Measure (Space d)inst✝¹:μ.HasTemperateGrowthinst✝:μ.IsOpenPosMeasureψ:↥(SchwartzSubmodule d μ)⊢ ⇑((schwartzEquiv μ).symm ψ) =ᵐ[μ] ↑↑↑ψ
  nth_rw 2 [← (schwartzEquiv μ).apply_symm_apply ψd:ℕμ:Measure (Space d)inst✝¹:μ.HasTemperateGrowthinst✝:μ.IsOpenPosMeasureψ:↥(SchwartzSubmodule d μ)⊢ ⇑((schwartzEquiv μ).symm ψ) =ᵐ[μ] ↑↑↑((schwartzEquiv μ) ((schwartzEquiv μ).symm ψ))]d:ℕμ:Measure (Space d)inst✝¹:μ.HasTemperateGrowthinst✝:μ.IsOpenPosMeasureψ:↥(SchwartzSubmodule d μ)⊢ ⇑((schwartzEquiv μ).symm ψ) =ᵐ[μ] ↑↑↑((schwartzEquiv μ) ((schwartzEquiv μ).symm ψ))
  exact (schwartzEquiv_coe_ae _).symmAll goals completed! 🐙lemma schwartzEquiv_ae_eq (h : schwartzEquiv μ f =ᵐ[μ] schwartzEquiv μ g) : f = g :=
  (EmbeddingLike.apply_eq_iff_eq _).mp (SetLike.coe_eq_coe.mp (ext_iff.mpr h))

A.2. Misc.

              

@[simp]
lemma zero_eq_top (μ : Measure (Space 0)) [μ.HasTemperateGrowth] [μ.IsOpenPosMeasure] :
    SchwartzSubmodule 0 μ = ⊤ := byμ:Measure (Space 0)inst✝¹:μ.HasTemperateGrowthinst✝:μ.IsOpenPosMeasure⊢ SchwartzSubmodule 0 μ = ⊤
  ext ψμ:Measure (Space 0)inst✝¹:μ.HasTemperateGrowthinst✝:μ.IsOpenPosMeasureψ:↥(SpaceDHilbertSpace 0 μ)⊢ ψ ∈ SchwartzSubmodule 0 μ ↔ ψ ∈ ⊤
  simp only [LinearMap.mem_range, ContinuousLinearMap.coe_coe, Submodule.mem_top, iff_true]μ:Measure (Space 0)inst✝¹:μ.HasTemperateGrowthinst✝:μ.IsOpenPosMeasureψ:↥(SpaceDHilbertSpace 0 μ)⊢ ∃ y, (schwartzIncl μ) y = ψ
  let g : 𝓢(Space 0, ℂ) := {
    toFun x := ψ 0
    smooth' := contDiff_const
    decay' k n := byμ:Measure (Space 0)inst✝¹:μ.HasTemperateGrowthinst✝:μ.IsOpenPosMeasureψ:↥(SpaceDHilbertSpace 0 μ)k:ℕn:ℕ⊢ ∃ C, ∀ (x : Space 0), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (fun x => ↑↑ψ 0) x‖ ≤ Cμ:Measure (Space 0)inst✝¹:μ.HasTemperateGrowthinst✝:μ.IsOpenPosMeasureψ:↥(SpaceDHilbertSpace 0 μ)g:𝓢(Space 0, ℂ) := { toFun := fun x => ↑↑ψ 0, smooth' := ⋯, decay' := ⋯ }⊢ ∃ y, (schwartzIncl μ) y = ψ
      refine ⟨‖ψ 0‖, fun x ↦ ?_⟩μ:Measure (Space 0)inst✝¹:μ.HasTemperateGrowthinst✝:μ.IsOpenPosMeasureψ:↥(SpaceDHilbertSpace 0 μ)k:ℕn:ℕx:Space 0⊢ ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (fun x => ↑↑ψ 0) x‖ ≤ ‖↑↑ψ 0‖μ:Measure (Space 0)inst✝¹:μ.HasTemperateGrowthinst✝:μ.IsOpenPosMeasureψ:↥(SpaceDHilbertSpace 0 μ)g:𝓢(Space 0, ℂ) := { toFun := fun x => ↑↑ψ 0, smooth' := ⋯, decay' := ⋯ }⊢ ∃ y, (schwartzIncl μ) y = ψ
      rcases eq_zero_or_pos n with rfl | hninlμ:Measure (Space 0)inst✝¹:μ.HasTemperateGrowthinst✝:μ.IsOpenPosMeasureψ:↥(SpaceDHilbertSpace 0 μ)k:ℕx:Space 0⊢ ‖x‖ ^ k * ‖iteratedFDeriv ℝ 0 (fun x => ↑↑ψ 0) x‖ ≤ ‖↑↑ψ 0‖inrμ:Measure (Space 0)inst✝¹:μ.HasTemperateGrowthinst✝:μ.IsOpenPosMeasureψ:↥(SpaceDHilbertSpace 0 μ)k:ℕn:ℕx:Space 0hn:0 < n⊢ ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (fun x => ↑↑ψ 0) x‖ ≤ ‖↑↑ψ 0‖μ:Measure (Space 0)inst✝¹:μ.HasTemperateGrowthinst✝:μ.IsOpenPosMeasureψ:↥(SpaceDHilbertSpace 0 μ)g:𝓢(Space 0, ℂ) := { toFun := fun x => ↑↑ψ 0, smooth' := ⋯, decay' := ⋯ }⊢ ∃ y, (schwartzIncl μ) y = ψ
      ·inlμ:Measure (Space 0)inst✝¹:μ.HasTemperateGrowthinst✝:μ.IsOpenPosMeasureψ:↥(SpaceDHilbertSpace 0 μ)k:ℕx:Space 0⊢ ‖x‖ ^ k * ‖iteratedFDeriv ℝ 0 (fun x => ↑↑ψ 0) x‖ ≤ ‖↑↑ψ 0‖μ:Measure (Space 0)inst✝¹:μ.HasTemperateGrowthinst✝:μ.IsOpenPosMeasureψ:↥(SpaceDHilbertSpace 0 μ)g:𝓢(Space 0, ℂ) := { toFun := fun x => ↑↑ψ 0, smooth' := ⋯, decay' := ⋯ }⊢ ∃ y, (schwartzIncl μ) y = ψ rw [← one_mul ‖ψ 0‖inlμ:Measure (Space 0)inst✝¹:μ.HasTemperateGrowthinst✝:μ.IsOpenPosMeasureψ:↥(SpaceDHilbertSpace 0 μ)k:ℕx:Space 0⊢ ‖x‖ ^ k * ‖iteratedFDeriv ℝ 0 (fun x => ↑↑ψ 0) x‖ ≤ 1 * ‖↑↑ψ 0‖inlμ:Measure (Space 0)inst✝¹:μ.HasTemperateGrowthinst✝:μ.IsOpenPosMeasureψ:↥(SpaceDHilbertSpace 0 μ)k:ℕx:Space 0⊢ ‖x‖ ^ k * ‖iteratedFDeriv ℝ 0 (fun x => ↑↑ψ 0) x‖ ≤ 1 * ‖↑↑ψ 0‖μ:Measure (Space 0)inst✝¹:μ.HasTemperateGrowthinst✝:μ.IsOpenPosMeasureψ:↥(SpaceDHilbertSpace 0 μ)g:𝓢(Space 0, ℂ) := { toFun := fun x => ↑↑ψ 0, smooth' := ⋯, decay' := ⋯ }⊢ ∃ y, (schwartzIncl μ) y = ψ]inlμ:Measure (Space 0)inst✝¹:μ.HasTemperateGrowthinst✝:μ.IsOpenPosMeasureψ:↥(SpaceDHilbertSpace 0 μ)k:ℕx:Space 0⊢ ‖x‖ ^ k * ‖iteratedFDeriv ℝ 0 (fun x => ↑↑ψ 0) x‖ ≤ 1 * ‖↑↑ψ 0‖μ:Measure (Space 0)inst✝¹:μ.HasTemperateGrowthinst✝:μ.IsOpenPosMeasureψ:↥(SpaceDHilbertSpace 0 μ)g:𝓢(Space 0, ℂ) := { toFun := fun x => ↑↑ψ 0, smooth' := ⋯, decay' := ⋯ }⊢ ∃ y, (schwartzIncl μ) y = ψ
        refine mul_le_mul ?_ (byμ:Measure (Space 0)inst✝¹:μ.HasTemperateGrowthinst✝:μ.IsOpenPosMeasureψ:↥(SpaceDHilbertSpace 0 μ)k:ℕx:Space 0⊢ ‖iteratedFDeriv ℝ 0 (fun x => ↑↑ψ 0) x‖ ≤ ‖↑↑ψ 0‖μ:Measure (Space 0)inst✝¹:μ.HasTemperateGrowthinst✝:μ.IsOpenPosMeasureψ:↥(SpaceDHilbertSpace 0 μ)g:𝓢(Space 0, ℂ) := { toFun := fun x => ↑↑ψ 0, smooth' := ⋯, decay' := ⋯ }⊢ ∃ y, (schwartzIncl μ) y = ψ simpAll goals completed! 🐙μ:Measure (Space 0)inst✝¹:μ.HasTemperateGrowthinst✝:μ.IsOpenPosMeasureψ:↥(SpaceDHilbertSpace 0 μ)g:𝓢(Space 0, ℂ) := { toFun := fun x => ↑↑ψ 0, smooth' := ⋯, decay' := ⋯ }⊢ ∃ y, (schwartzIncl μ) y = ψ) (norm_nonneg _) zero_le_one
        simp [Space.point_dim_zero_eq, zero_pow_le_one]All goals completed! 🐙μ:Measure (Space 0)inst✝¹:μ.HasTemperateGrowthinst✝:μ.IsOpenPosMeasureψ:↥(SpaceDHilbertSpace 0 μ)g:𝓢(Space 0, ℂ) := { toFun := fun x => ↑↑ψ 0, smooth' := ⋯, decay' := ⋯ }⊢ ∃ y, (schwartzIncl μ) y = ψ
      ·inrμ:Measure (Space 0)inst✝¹:μ.HasTemperateGrowthinst✝:μ.IsOpenPosMeasureψ:↥(SpaceDHilbertSpace 0 μ)k:ℕn:ℕx:Space 0hn:0 < n⊢ ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (fun x => ↑↑ψ 0) x‖ ≤ ‖↑↑ψ 0‖μ:Measure (Space 0)inst✝¹:μ.HasTemperateGrowthinst✝:μ.IsOpenPosMeasureψ:↥(SpaceDHilbertSpace 0 μ)g:𝓢(Space 0, ℂ) := { toFun := fun x => ↑↑ψ 0, smooth' := ⋯, decay' := ⋯ }⊢ ∃ y, (schwartzIncl μ) y = ψ simp [iteratedFDeriv_const_of_ne hn.ne']All goals completed! 🐙μ:Measure (Space 0)inst✝¹:μ.HasTemperateGrowthinst✝:μ.IsOpenPosMeasureψ:↥(SpaceDHilbertSpace 0 μ)g:𝓢(Space 0, ℂ) := { toFun := fun x => ↑↑ψ 0, smooth' := ⋯, decay' := ⋯ }⊢ ∃ y, (schwartzIncl μ) y = ψ
  }μ:Measure (Space 0)inst✝¹:μ.HasTemperateGrowthinst✝:μ.IsOpenPosMeasureψ:↥(SpaceDHilbertSpace 0 μ)g:𝓢(Space 0, ℂ) := { toFun := fun x => ↑↑ψ 0, smooth' := ⋯, decay' := ⋯ }⊢ ∃ y, (schwartzIncl μ) y = ψ
  use ghμ:Measure (Space 0)inst✝¹:μ.HasTemperateGrowthinst✝:μ.IsOpenPosMeasureψ:↥(SpaceDHilbertSpace 0 μ)g:𝓢(Space 0, ℂ) := { toFun := fun x => ↑↑ψ 0, smooth' := ⋯, decay' := ⋯ }⊢ (schwartzIncl μ) g = ψ
  exthμ:Measure (Space 0)inst✝¹:μ.HasTemperateGrowthinst✝:μ.IsOpenPosMeasureψ:↥(SpaceDHilbertSpace 0 μ)g:𝓢(Space 0, ℂ) := { toFun := fun x => ↑↑ψ 0, smooth' := ⋯, decay' := ⋯ }⊢ ↑↑((schwartzIncl μ) g) =ᵐ[μ] ↑↑ψ
  filter_upwards [schwartzEquiv_coe_ae g] with x hgμ:Measure (Space 0)inst✝¹:μ.HasTemperateGrowthinst✝:μ.IsOpenPosMeasureψ:↥(SpaceDHilbertSpace 0 μ)g:𝓢(Space 0, ℂ) := { toFun := fun x => ↑↑ψ 0, smooth' := ⋯, decay' := ⋯ }x:Space 0hg:↑↑↑((schwartzEquiv μ) g) x = g x⊢ ↑↑((schwartzIncl μ) g) x = ↑↑ψ x
  rw [← schwartzEquiv_apply_coe,μ:Measure (Space 0)inst✝¹:μ.HasTemperateGrowthinst✝:μ.IsOpenPosMeasureψ:↥(SpaceDHilbertSpace 0 μ)g:𝓢(Space 0, ℂ) := { toFun := fun x => ↑↑ψ 0, smooth' := ⋯, decay' := ⋯ }x:Space 0hg:↑↑↑((schwartzEquiv μ) g) x = g x⊢ ↑↑↑((schwartzEquiv μ) g) x = ↑↑ψ xμ:Measure (Space 0)inst✝¹:μ.HasTemperateGrowthinst✝:μ.IsOpenPosMeasureψ:↥(SpaceDHilbertSpace 0 μ)g:𝓢(Space 0, ℂ) := { toFun := fun x => ↑↑ψ 0, smooth' := ⋯, decay' := ⋯ }x:Space 0hg:↑↑↑((schwartzEquiv μ) g) x = g x⊢ g 0 = ↑↑ψ 0 hg,μ:Measure (Space 0)inst✝¹:μ.HasTemperateGrowthinst✝:μ.IsOpenPosMeasureψ:↥(SpaceDHilbertSpace 0 μ)g:𝓢(Space 0, ℂ) := { toFun := fun x => ↑↑ψ 0, smooth' := ⋯, decay' := ⋯ }x:Space 0hg:↑↑↑((schwartzEquiv μ) g) x = g x⊢ g x = ↑↑ψ xμ:Measure (Space 0)inst✝¹:μ.HasTemperateGrowthinst✝:μ.IsOpenPosMeasureψ:↥(SpaceDHilbertSpace 0 μ)g:𝓢(Space 0, ℂ) := { toFun := fun x => ↑↑ψ 0, smooth' := ⋯, decay' := ⋯ }x:Space 0hg:↑↑↑((schwartzEquiv μ) g) x = g x⊢ g 0 = ↑↑ψ 0 Space.point_dim_zero_eq xμ:Measure (Space 0)inst✝¹:μ.HasTemperateGrowthinst✝:μ.IsOpenPosMeasureψ:↥(SpaceDHilbertSpace 0 μ)g:𝓢(Space 0, ℂ) := { toFun := fun x => ↑↑ψ 0, smooth' := ⋯, decay' := ⋯ }x:Space 0hg:↑↑↑((schwartzEquiv μ) g) x = g x⊢ g 0 = ↑↑ψ 0μ:Measure (Space 0)inst✝¹:μ.HasTemperateGrowthinst✝:μ.IsOpenPosMeasureψ:↥(SpaceDHilbertSpace 0 μ)g:𝓢(Space 0, ℂ) := { toFun := fun x => ↑↑ψ 0, smooth' := ⋯, decay' := ⋯ }x:Space 0hg:↑↑↑((schwartzEquiv μ) g) x = g x⊢ g 0 = ↑↑ψ 0]μ:Measure (Space 0)inst✝¹:μ.HasTemperateGrowthinst✝:μ.IsOpenPosMeasureψ:↥(SpaceDHilbertSpace 0 μ)g:𝓢(Space 0, ℂ) := { toFun := fun x => ↑↑ψ 0, smooth' := ⋯, decay' := ⋯ }x:Space 0hg:↑↑↑((schwartzEquiv μ) g) x = g x⊢ g 0 = ↑↑ψ 0
  rflAll goals completed! 🐙lemma schwartzEquiv_inner :
    ⟪schwartzEquiv μ f, schwartzEquiv μ g⟫_ℂ = ∫ x, starRingEnd ℂ (f x) * g x ∂μ := byd:ℕμ:Measure (Space d)inst✝¹:μ.HasTemperateGrowthinst✝:μ.IsOpenPosMeasuref:𝓢(Space d, ℂ)g:𝓢(Space d, ℂ)⊢ ⟪(schwartzEquiv μ) f, (schwartzEquiv μ) g⟫_ℂ = ∫ (x : Space d), (starRingEnd ℂ) (f x) * g x ∂μ
  apply integral_congr_aed:ℕμ:Measure (Space d)inst✝¹:μ.HasTemperateGrowthinst✝:μ.IsOpenPosMeasuref:𝓢(Space d, ℂ)g:𝓢(Space d, ℂ)⊢ (fun a =>
    ⟪↑↑((SchwartzSubmodule d μ).subtype ((schwartzEquiv μ) f)) a,
      ↑↑((SchwartzSubmodule d μ).subtype ((schwartzEquiv μ) g)) a⟫_ℂ) =ᵐ[μ]
  fun a => (starRingEnd ℂ) (f a) * g a
  filter_upwards [schwartzEquiv_coe_ae f, schwartzEquiv_coe_ae g] with _ hfd:ℕμ:Measure (Space d)inst✝¹:μ.HasTemperateGrowthinst✝:μ.IsOpenPosMeasuref:𝓢(Space d, ℂ)g:𝓢(Space d, ℂ)a✝:Space dhf:↑↑↑((schwartzEquiv μ) f) a✝ = f a✝⊢ ↑↑↑((schwartzEquiv μ) g) a✝ = g a✝ →
  ⟪↑↑((SchwartzSubmodule d μ).subtype ((schwartzEquiv μ) f)) a✝,
      ↑↑((SchwartzSubmodule d μ).subtype ((schwartzEquiv μ) g)) a✝⟫_ℂ =
    (starRingEnd ℂ) (f a✝) * g a✝ hgd:ℕμ:Measure (Space d)inst✝¹:μ.HasTemperateGrowthinst✝:μ.IsOpenPosMeasuref:𝓢(Space d, ℂ)g:𝓢(Space d, ℂ)a✝:Space dhf:↑↑↑((schwartzEquiv μ) f) a✝ = f a✝hg:↑↑↑((schwartzEquiv μ) g) a✝ = g a✝⊢ ⟪↑↑((SchwartzSubmodule d μ).subtype ((schwartzEquiv μ) f)) a✝,
    ↑↑((SchwartzSubmodule d μ).subtype ((schwartzEquiv μ) g)) a✝⟫_ℂ =
  (starRingEnd ℂ) (f a✝) * g a✝
  simp [hf, hg, mul_comm]All goals completed! 🐙omit [μ.IsOpenPosMeasure] in
lemma toTemperedDistribution_schwartzIncl_eq :
    toTemperedDistribution (schwartzIncl μ g) = g.toTemperedDistributionCLM (Space d) ℂ μ :=
  Lp.toTemperedDistribution_toLp_eq g

B. SchwartzSubmoduleOn

The projection of SchwartzSubmodule d μ onto SpaceDHilbertSpaceOn Ω μ.

abbrev SchwartzSubmoduleOn
    {d : ℕ} (Ω : Set (Space d)) (μ : Measure (Space d) := volume) [μ.HasTemperateGrowth] :
    Submodule ℂ (SpaceDHilbertSpaceOn Ω μ) :=
  (SchwartzSubmodule d μ).map (subspaceProjection Ω μ)