1. Physlib
  2. QuantumMechanics
  3. HilbertSpaces
  4. SpaceD
  5. SobolevSubmodule
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.Distribution.Sobolev public import Physlib.QuantumMechanics.HilbertSpaces.SpaceD.SchwartzSubmodule

Sobolev submodules of SpaceDHilbertSpace

i. Overview

In this module we define the Sobolev submodules of SpaceDHilbertSpace.

ii. Key results

    SobolevSubmodule d s : the Sobolev space H^s as a submodule of SpaceDHilbertSpace d.

    SobolevSubmodule.schwartzIncl_mem / schwartzSubmodule_le_sobolevSubmodule / SobolevSubmodule.dense : Schwartz maps lie in every H^s, which is therefore dense.

    SobolevSubmodule.antitone : H^s ≀ H^s' for s' ≀ s.

iii. Table of contents

    A. The Sobolev submodule H^s

iv. References

@[expose] public section

A. The Sobolev submodule H^s

The Sobolev space H^s as a submodule of SpaceDHilbertSpace d: the LΒ² classes whose associated tempered distribution satisfies MemSobolev s 2.

def SobolevSubmodule (d : β„•) (s : ℝ) : Submodule β„‚ (SpaceDHilbertSpace d) where carrier := {ψ | MemSobolev s 2 (toTemperedDistributionCLM d volume ψ)} add_mem' {ψ Ο†} hψ hΟ† := d✝:β„•ΞΌ:Measure (Space d✝)inst✝:ΞΌ.HasTemperateGrowthd:β„•s:β„Οˆ:β†₯(SpaceDHilbertSpace d)Ο†:β†₯(SpaceDHilbertSpace d)hψ:ψ ∈ {ψ | MemSobolev s 2 ((toTemperedDistributionCLM d volume) ψ)}hΟ†:Ο† ∈ {ψ | MemSobolev s 2 ((toTemperedDistributionCLM d volume) ψ)}⊒ ψ + Ο† ∈ {ψ | MemSobolev s 2 ((toTemperedDistributionCLM d volume) ψ)} All goals completed! πŸ™ zero_mem' := d✝:β„•ΞΌ:Measure (Space d✝)inst✝:ΞΌ.HasTemperateGrowthd:β„•s:β„βŠ’ 0 ∈ {ψ | MemSobolev s 2 ((toTemperedDistributionCLM d volume) ψ)} All goals completed! πŸ™ smul_mem' c ψ hψ := d✝:β„•ΞΌ:Measure (Space d✝)inst✝:ΞΌ.HasTemperateGrowthd:β„•s:ℝc:β„‚Οˆ:β†₯(SpaceDHilbertSpace d)hψ:ψ ∈ {ψ | MemSobolev s 2 ((toTemperedDistributionCLM d volume) ψ)}⊒ c β€’ ψ ∈ {ψ | MemSobolev s 2 ((toTemperedDistributionCLM d volume) ψ)} All goals completed! πŸ™

Membership in H^s is the Sobolev condition on the associated tempered distribution.

lemma mem_sobolevSubmodule_iff {s : ℝ} {ψ : SpaceDHilbertSpace d} : ψ ∈ SobolevSubmodule d s ↔ MemSobolev s 2 (toTemperedDistribution ψ) := Iff.rfl

Schwartz maps lie in every Sobolev space H^s.

d:β„•s:ℝg:𝓒(Space d, β„‚)⊒ MemSobolev s 2 ((SchwartzMap.toTemperedDistributionCLM (Space d) β„‚ volume) g) All goals completed! πŸ™

The Schwartz submodule is contained in every Sobolev space H^s.

lemma schwartzSubmodule_le_sobolevSubmodule (s : ℝ) : SchwartzSubmodule d ≀ SobolevSubmodule d s := d:β„•s:β„βŠ’ SchwartzSubmodule d volume ≀ SobolevSubmodule d s d:β„•s:ℝg:𝓒(Space d, β„‚)⊒ ↑(schwartzIncl volume) g ∈ SobolevSubmodule d s All goals completed! πŸ™

Every Sobolev space H^s is dense in SpaceDHilbertSpace d, containing the dense Schwartz submodule.

lemma SobolevSubmodule.dense (s : ℝ) : Dense (SobolevSubmodule d s : Set (SpaceDHilbertSpace d)) := (SchwartzSubmodule.dense d volume).mono (schwartzSubmodule_le_sobolevSubmodule s)

The Sobolev spaces shrink as the regularity index grows: H^s ≀ H^s' for s' ≀ s.

lemma SobolevSubmodule.antitone (d : β„•) : Antitone (SobolevSubmodule d) := fun _ _ h _ hψ => hψ.mono h