1. Physlib
  2. QuantumMechanics
  3. HilbertSpaces
  4. SpaceD
  5. Fourier
Imports
/- Copyright (c) 2026 Adam Bornemann. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Adam Bornemann -/ module public import Mathlib.Analysis.Fourier.LpSpace public import Physlib.QuantumMechanics.HilbertSpaces.SpaceD.SchwartzSubmodule

The Fourier transform on SpaceDHilbertSpace

i. Overview

In this module we define the Fourier transform on SpaceDHilbertSpace d as a unitary operator. Mathlib's LΒ² Fourier transform MeasureTheory.Lp.fourierTransformβ‚—α΅’ is a linear isometry equivalence of Lp β„‚ 2 volume, hence of SpaceDHilbertSpace d, onto itself; packaged as fourierUnitary d.

ii. Key results

    fourierUnitary d : the LΒ² Fourier transform as a unitary SpaceDHilbertSpace d ≃ₗᡒ[β„‚] SpaceDHilbertSpace d, acting as 𝓕/𝓕⁻ (fourierUnitary_apply, fourierUnitary_symm_apply).

    schwartzIncl_fourier_eq : 𝓕 (schwartzIncl f) = schwartzIncl (𝓕 f).

    schwartzIncl_fourierInv_eq : the inverse acts by the inverse Schwartz Fourier transform.

    fourierUnitary_map_schwartzSubmodule : fourierUnitary d maps the Schwartz submodule onto itself.

iii. Table of contents

    A. The Fourier unitary

    B. Action on the Schwartz submodule

iv. References

@[expose] public section

A. The Fourier unitary

fourierUnitary d acts as the LΒ² Fourier transform 𝓕.

@[simp] lemma fourierUnitary_apply (ψ : SpaceDHilbertSpace d) : fourierUnitary d ψ = 𝓕 ψ := rfl

(fourierUnitary d).symm acts as the inverse LΒ² Fourier transform 𝓕⁻.

@[simp] lemma fourierUnitary_symm_apply (ψ : SpaceDHilbertSpace d) : (fourierUnitary d).symm ψ = 𝓕⁻ ψ := rfl

B. Action on the Schwartz submodule

Applying fourierUnitary d to the LΒ² class of a Schwartz map f gives the LΒ² class of the Schwartz Fourier transform 𝓕 f.

lemma schwartzIncl_fourier_eq (f : 𝓒(Space d, β„‚)) : 𝓕 (schwartzIncl volume f) = schwartzIncl volume (𝓕 f) := SchwartzMap.toLp_fourier_eq f

Applying 𝓕⁻ to the LΒ² class of a Schwartz map f gives the LΒ² class of the inverse Schwartz Fourier transform 𝓕⁻ f.

lemma schwartzIncl_fourierInv_eq (f : 𝓒(Space d, β„‚)) : 𝓕⁻ (schwartzIncl volume f) = schwartzIncl volume (𝓕⁻ f) := SchwartzMap.toLp_fourierInv_eq f

Pulling the LΒ² class of 𝓕 f back through the Fourier unitary recovers the LΒ² class of f.

All goals completed! πŸ™

The Fourier unitary maps the Schwartz submodule onto itself.

lemma fourierUnitary_map_schwartzSubmodule : (SchwartzSubmodule d).map (fourierUnitary d).toLinearMap = SchwartzSubmodule d := d:β„•βŠ’ Submodule.map (↑(fourierUnitary d).toLinearEquiv) (SchwartzSubmodule d volume) = SchwartzSubmodule d volume d:β„•βŠ’ Submodule.map (↑(fourierUnitary d).toLinearEquiv) (SchwartzSubmodule d volume) ≀ SchwartzSubmodule d volumed:β„•βŠ’ SchwartzSubmodule d volume ≀ Submodule.map (↑(fourierUnitary d).toLinearEquiv) (SchwartzSubmodule d volume) d:β„•βŠ’ Submodule.map (↑(fourierUnitary d).toLinearEquiv) (SchwartzSubmodule d volume) ≀ SchwartzSubmodule d volume d:β„•f:𝓒(Space d, β„‚)⊒ ↑(fourierUnitary d).toLinearEquiv (↑(schwartzIncl volume) f) ∈ SchwartzSubmodule d volume All goals completed! πŸ™ d:β„•βŠ’ SchwartzSubmodule d volume ≀ Submodule.map (↑(fourierUnitary d).toLinearEquiv) (SchwartzSubmodule d volume) d:β„•g:𝓒(Space d, β„‚)⊒ ↑(schwartzIncl volume) g ∈ Submodule.map (↑(fourierUnitary d).toLinearEquiv) (SchwartzSubmodule d volume) exact βŸ¨π“•β» (schwartzIncl volume g), βŸ¨π“•β» g, (schwartzIncl_fourierInv_eq g).symm⟩, d:β„•g:𝓒(Space d, β„‚)⊒ ↑(fourierUnitary d).toLinearEquiv (𝓕⁻ ((schwartzIncl volume) g)) = ↑(schwartzIncl volume) g All goals completed! πŸ™βŸ©