feat(QuantumMechanics): derivative operators via Fourier-conjugated m…

Physlib.lean

@@ -303,6 +303,7 @@ public import Physlib.QuantumMechanics.InfiniteSquareWell.Basic
 public import Physlib.QuantumMechanics.Operators.AngularMomentum
 public import Physlib.QuantumMechanics.Operators.Commutation
 public import Physlib.QuantumMechanics.Operators.Covariance
+public import Physlib.QuantumMechanics.Operators.Derivative
 public import Physlib.QuantumMechanics.Operators.Examples
 public import Physlib.QuantumMechanics.Operators.Momentum
 public import Physlib.QuantumMechanics.Operators.Multiplication

Physlib/QuantumMechanics/Operators/Derivative.lean

@@ -0,0 +1,139 @@
+/-
+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 Physlib.QuantumMechanics.HilbertSpaces.SpaceD.Fourier
+public import Physlib.QuantumMechanics.Operators.Multiplication
+public import Physlib.QuantumMechanics.Operators.SpectralTheory.SelfAdjoint
+/-!
+
+# Derivative operators
+
+## i. Overview
+
+Every constant-coefficient differential operator is unitarily equivalent, via the Fourier transform,
+to a multiplication operator. In this module we take that as a definition: for a symbol
+`f : Space d → ℂ`, a function of the wavenumber `k`, the derivative operator `derivOperator f` is
+the conjugate `𝓕⁻¹ ∘ 𝓜 (f ∘ 2π•) ∘ 𝓕` of the multiplication operator by the Fourier unitary,
+through `LinearPMap.unitaryConj`.
+
+The explicit factors of `2π` implement the change of variables between mathlib's Fourier
+convention and the physics one: mathlib's `𝓕` pairs position with the frequency `ξ` through
+`e^(-2πi ⟨x, ξ⟩)`, while physics symbols are written in the wavenumber `k = 2πξ`. Rather than
+introduce a rescaled transform, we rescale the symbol once and for all: `derivOperator f`
+multiplies `𝓕ψ` at frequency `ξ` by `f (2πξ)`, so `f` itself is always a function of the
+wavenumber.
+
+## ii. Key results
+
+- `derivOperator` : the derivative operator with wavenumber symbol `f`, with notation `𝓓 f`.
+- `derivOperator_hasDenseDomain` : it is densely defined for a.e.-strongly-measurable `f`.
+- `derivOperator_adjoint` : its adjoint is the derivative operator of the conjugate symbol.
+- `derivOperator_isSelfAdjoint` : it is self-adjoint for real-valued `f`.
+- `schwartzSubmodule_le_derivOperator_domain` : the Schwartz submodule lies in the domain for
+    temperate-growth `f`.
+
+## iii. Table of contents
+
+- A. Definitions
+- B. Basic properties
+  - B.1. Domain
+  - B.2. Adjoints
+
+## iv. References
+
+-/
+
+@[expose] public section
+
+namespace QuantumMechanics
+namespace SpaceDHilbertSpace
+noncomputable section
+
+open MeasureTheory ComplexConjugate
+open LinearPMap Real FourierTransform
+
+/-!
+## A. Definition
+-/
+
+variable {d : ℕ} {f : Space d → ℂ}
+
+/-- The derivative operator with symbol `f : Space d → ℂ`, interpreted as a function of the
+wavenumber `k`. -/
+def derivOperator (f : Space d → ℂ) : SpaceDHilbertSpace d →ₗ.[ℂ] SpaceDHilbertSpace d :=
+  (𝓜 volume (f ∘ fun k ↦ (2 * π) • k)).unitaryConj (fourierUnitary d).symm
+
+@[inherit_doc derivOperator]
+notation "𝓓" => derivOperator
+
+/-- The defining equation: `𝓓 f` is the multiplication operator by the rescaled symbol
+`f ∘ 2π•`, conjugated through the inverse Fourier unitary. -/
+lemma derivOperator_eq (f : Space d → ℂ) :
+    𝓓 f = (𝓜 volume (f ∘ fun k ↦ (2 * π) • k)).unitaryConj (fourierUnitary d).symm := rfl
+
+/-- a.e.-strong measurability of symbols is preserved under composition with scalar
+multiplication: nonzero scaling is quasi-measure-preserving for the Haar measure, and zero
+scaling gives a constant function. -/
+lemma aestronglyMeasurable_comp_const_smul {μ : Measure (Space d)} [μ.IsAddHaarMeasure]
+    (hf : AEStronglyMeasurable f μ) (c : ℝ) :
+    AEStronglyMeasurable (f ∘ fun k ↦ c • k) μ := by
+  rcases eq_or_ne c 0 with rfl | hc
+  · simpa [Function.comp_def] using aestronglyMeasurable_const
+  · exact hf.comp_quasiMeasurePreserving
+      ⟨measurable_const_smul _, by
+        rw [Measure.map_addHaar_smul μ hc]
+        exact Measure.smul_absolutelyContinuous⟩
+
+/-- Membership: `ψ ∈ D(𝓓 f)` iff `𝓕ψ` lies in the domain of multiplication by the
+rescaled symbol. -/
+lemma mem_derivOperator_domain_iff {ψ : SpaceDHilbertSpace d} :
+    ψ ∈ (𝓓 f).domain ↔ 𝓕 ψ ∈ (𝓜 volume (f ∘ fun k ↦ (2 * π) • k)).domain := Iff.rfl
+
+/-- The defining formula: `𝓓 f ψ = 𝓕⁻¹ ((f ∘ 2π•) · 𝓕ψ)`. -/
+lemma derivOperator_apply (ψ : (𝓓 f).domain) :
+    𝓓 f ψ =
+      𝓕⁻ ((𝓜 volume (f ∘ fun k ↦ (2 * π) • k)) ⟨𝓕 ψ.1, mem_derivOperator_domain_iff.mp ψ.2⟩) := rfl
+
+/-!
+## B.1. Domain
+-/
+
+/-- The derivative operator is densely defined. -/
+lemma derivOperator_hasDenseDomain (hf : AEStronglyMeasurable f volume) :
+    (𝓓 f).HasDenseDomain :=
+  (mulOperator_hasDenseDomain
+    (aestronglyMeasurable_comp_const_smul hf (2 * π))).unitaryConj_dense_domain
+
+/-- For a temperate-growth symbol the Schwartz submodule lies in the domain of the derivative
+operator. -/
+lemma schwartzSubmodule_le_derivOperator_domain (hf : f.HasTemperateGrowth) :
+    SchwartzSubmodule d ≤ (𝓓 f).domain :=
+  fun _ hψ => mem_derivOperator_domain_iff.mpr
+    (mulOperator_domain_ge_of_hasTemperateGrowth (by fun_prop) volume
+      (fourierUnitary_map_schwartzSubmodule ▸ Submodule.mem_map_of_mem hψ))
+
+/-!
+## B.2. Adjoints
+-/
+
+/-- The adjoint of a derivative operator is the derivative operator of the conjugate symbol:
+`(𝓓 f)† = 𝓓 (conj ∘ f)`. -/
+lemma derivOperator_adjoint (hf : AEStronglyMeasurable f volume) :
+    (𝓓 f)† = 𝓓 (conj ∘ f) := by
+  simp only [derivOperator_eq, aestronglyMeasurable_comp_const_smul hf, unitaryConj_adjoint,
+    mulOperator_adjoint_eq_conj, Function.comp_assoc]
+
+/-- The derivative operator of a real-valued symbol is self-adjoint on its maximal domain. -/
+lemma derivOperator_isSelfAdjoint (hf : AEStronglyMeasurable f volume)
+    (hf' : conj ∘ f = f) : IsSelfAdjoint (𝓓 f) :=
+  LinearPMap.unitaryConj_isSelfAdjoint (fourierUnitary d).symm
+    (mulOperator_isSelfAdjoint_ofReal (aestronglyMeasurable_comp_const_smul hf (2 * π))
+      (funext fun ξ => congrFun hf' ((2 * π) • ξ)))
+
+end
+end SpaceDHilbertSpace
+end QuantumMechanics

Physlib/QuantumMechanics/Operators/Unbounded.lean

@@ -620,6 +620,25 @@ lemma unitaryConj_apply_map (y : A.domain) :
     unitaryConj u A ⟨u (y : H), map_mem_unitaryConj_domain u A y⟩ = u (A y) := by
   simp only [unitaryConj_apply, u.symm_apply_apply]
 
+/-- Unitary conjugation is monotone for the extension order on partial linear maps. -/
+lemma unitaryConj_mono (u : H ≃ₗᵢ[ℂ] H') {A B : H →ₗ.[ℂ] H} (h : A ≤ B) :
+    unitaryConj u A ≤ unitaryConj u B :=
+  ⟨fun _ hx => h.1 hx, fun x y hxy =>
+    congrArg u (h.2 (x := ⟨u.symm ↑x, x.2⟩) (y := ⟨u.symm ↑y, y.2⟩) (congrArg u.symm hxy))⟩
+
+/-- Conjugating by `u` and then by `u⁻¹` recovers the original operator. -/
+@[simp]
+lemma unitaryConj_symm_unitaryConj (u : H ≃ₗᵢ[ℂ] H') (A : H →ₗ.[ℂ] H) :
+    unitaryConj u.symm (unitaryConj u A) = A := by
+  ext x hx hx'
+  · simp [mem_unitaryConj_domain_iff]
+  · simp [unitaryConj_apply]
+
+/-- Conjugating by `u⁻¹` and then by `u` recovers the original operator. -/
+@[simp]
+lemma unitaryConj_unitaryConj_symm (u : H ≃ₗᵢ[ℂ] H') (B : H' →ₗ.[ℂ] H') :
+    unitaryConj u (unitaryConj u.symm B) = B := unitaryConj_symm_unitaryConj u.symm B
+
 variable {u A}
 
 open scoped InnerProductSpace in
@@ -640,6 +659,53 @@ preimage of a dense set under a homeomorphism. -/
 lemma HasDenseDomain.unitaryConj_dense_domain (hdense : A.HasDenseDomain) :
     (unitaryConj u A).HasDenseDomain := hdense.preimage u.symm.toHomeomorph.isOpenMap
 
+/-- The conjugated operator `u A u⁻¹` is densely defined iff `A` is: its domain is the preimage
+of `D(A)` under the homeomorphism `u⁻¹`. -/
+@[simp]
+lemma unitaryConj_hasDenseDomain_iff :
+    (unitaryConj u A).HasDenseDomain ↔ A.HasDenseDomain :=
+  ⟨fun h ↦ by simpa using h.unitaryConj_dense_domain (u := u.symm),
+   fun h ↦ h.unitaryConj_dense_domain⟩
+
+/-- Unitary conjugation commutes with the adjoint: `(u A u⁻¹)† = u A† u⁻¹`. -/
+@[simp]
+lemma unitaryConj_adjoint [CompleteSpace H] [CompleteSpace H'] (u : H ≃ₗᵢ[ℂ] H') :
+    (unitaryConj u A)† = unitaryConj u A† := by
+  by_cases hdense : A.HasDenseDomain
+  · have hd' : (unitaryConj u A).HasDenseDomain := hdense.unitaryConj_dense_domain
+    refine le_antisymm ?_ (((adjoint_isFormalAdjoint hdense).symm.unitaryConj).le_adjoint hd')
+    have h₁ : unitaryConj u.symm ((unitaryConj u A)†) ≤ (unitaryConj u.symm (unitaryConj u A))† :=
+      ((adjoint_isFormalAdjoint hd').symm.unitaryConj).le_adjoint hd'.unitaryConj_dense_domain
+    rw [unitaryConj_symm_unitaryConj] at h₁
+    have h₂ := unitaryConj_mono u h₁
+    rwa [unitaryConj_unitaryConj_symm] at h₂
+  · have hnd : ¬(unitaryConj u A).HasDenseDomain :=
+      fun hc ↦ hdense (unitaryConj_hasDenseDomain_iff.mp hc)
+    refine dExt ?_ fun x y hxy ↦ ?_
+    · ext ξ
+      change Continuous (fun w : (unitaryConj u A).domain ↦ ⟪ξ, unitaryConj u A w⟫_ℂ)
+        ↔ Continuous (fun w : A.domain ↦ ⟪u.symm ξ, A w⟫_ℂ)
+      constructor
+      · intro hc
+        suffices hfun : (fun w : A.domain ↦ ⟪u.symm ξ, A w⟫_ℂ)
+            = (fun w : (unitaryConj u A).domain ↦ ⟪ξ, unitaryConj u A w⟫_ℂ)
+              ∘ fun w : A.domain ↦ (⟨u ↑w, map_mem_unitaryConj_domain u A w⟩ :
+                (unitaryConj u A).domain) by
+          rw [hfun]
+          exact hc.comp ((u.continuous.comp continuous_subtype_val).subtype_mk _)
+        funext w
+        simp [unitaryConj_apply_map, u.symm.inner_map_eq_flip]
+      · intro hc
+        suffices hfun : (fun w : (unitaryConj u A).domain ↦ ⟪ξ, unitaryConj u A w⟫_ℂ)
+            = (fun w : A.domain ↦ ⟪u.symm ξ, A w⟫_ℂ)
+              ∘ fun w : (unitaryConj u A).domain ↦ (⟨u.symm ↑w, w.2⟩ : A.domain) by
+          rw [hfun]
+          exact hc.comp ((u.symm.continuous.comp continuous_subtype_val).subtype_mk _)
+        funext w
+        simp [unitaryConj_apply, u.symm.inner_map_eq_flip]
+    · simp [adjoint_apply_of_not_dense hnd x, unitaryConj_apply,
+        adjoint_apply_of_not_dense hdense]
+
 /-- If `A - z` is surjective for a scalar `z : ℂ`, then so is `u A u⁻¹ - z`. -/
 lemma unitaryConj_sub_smul_surjective {z : ℂ} (h : Function.Surjective (A - z • 1).toFun) :
     Function.Surjective (unitaryConj u A - z • 1).toFun := by