Imports
/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module
public import Mathlib.Analysis.InnerProductSpace.Dual
public import Mathlib.MeasureTheory.Function.L2Space
public import Mathlib.MeasureTheory.Measure.Haar.OfBasis
public import Physlib.Meta.TODO.BasicHilbert space for one dimension quantum mechanics
TODO "Remove 1d Hilbert space once dependencies are moved over to SpaceDHilbertSpace."@[expose] public section
The Hilbert space for a one dimensional quantum system is defined as
the space of almost-everywhere equal equivalence classes of square integrable functions
from ℝ to ℂ.
abbrev HilbertSpace := MeasureTheory.Lp (α := ℝ) ℂ 2The anti-linear map from the Hilbert space to it's dual.
def toBra : HilbertSpace →ₛₗ[starRingEnd ℂ] StrongDual ℂ HilbertSpace :=
InnerProductSpace.toDual ℂ HilbertSpace@[simp] lemma toBra_apply (f g : HilbertSpace) : toBra f g = ⟪f, g⟫_ℂ := rfl
The anti-linear map, toBra, taking a ket to it's corresponding
bra is surjective.
lemma toBra_surjective : Function.Surjective toBra :=
(InnerProductSpace.toDual ℂ HilbertSpace).surjective
The anti-linear map, toBra, taking a ket to it's corresponding
bra is injective.
lemma toBra_injective : Function.Injective toBra := ⊢ Function.Injective ⇑toBra
f:↥HilbertSpaceg:↥HilbertSpaceh:toBra f = toBra g⊢ f = g
All goals completed! 🐙Member of the Hilbert space as a property
The proposition MemHS f for a function f : ℝ → ℂ is defined
to be true if the function f can be lifted to the Hilbert space.
def MemHS (f : ℝ → ℂ) : Prop := MemLp f 2 MeasureTheory.volumelemma aeStronglyMeasurable_of_memHS {f : ℝ → ℂ} (h : MemHS f) : AEStronglyMeasurable f := h.1
A function f satisfies MemHS f if and only if it is almost everywhere
strongly measurable, and square integrable.
f:ℝ → ℂh1:AEStronglyMeasurable f volume⊢ ∫⁻ (a : ℝ), ‖f a‖ₑ ^ ENNReal.toReal 2 < ⊤ ↔ Integrable (fun x => ‖f x‖ ^ 2) volume
f:ℝ → ℂh1:AEStronglyMeasurable f volume⊢ ∫⁻ (a : ℝ), ‖f a‖ₑ ^ 2 < ⊤ ↔
AEStronglyMeasurable (fun x => ‖f x‖ ^ 2) volume ∧ HasFiniteIntegral (fun x => ‖f x‖ ^ 2) volume
f:ℝ → ℂh1:AEStronglyMeasurable f volumeh0:AEStronglyMeasurable (fun x => ‖f x‖ ^ 2) volume⊢ ∫⁻ (a : ℝ), ‖f a‖ₑ ^ 2 < ⊤ ↔
AEStronglyMeasurable (fun x => ‖f x‖ ^ 2) volume ∧ HasFiniteIntegral (fun x => ‖f x‖ ^ 2) volume
All goals completed! 🐙⊢ AEStronglyMeasurable (fun x => 0) volume ∧ Integrable (fun x => ‖0‖ ^ 2) volume
⊢ AEStronglyMeasurable (fun x => 0) volume
All goals completed! 🐙@[simp]
lemma zero_fun_memHS : MemHS (fun _ : ℝ => (0 : ℂ)) := zero_memHSlemma memHS_add {f g : ℝ → ℂ} (hf : MemHS f) (hg : MemHS g) :
MemHS (f + g) := MeasureTheory.MemLp.add hf hglemma memHS_smul {f : ℝ → ℂ} {c : ℂ} (hf : MemHS f) :
MemHS (c • f) := MeasureTheory.MemLp.const_smul hf clemma memHS_of_ae {g : ℝ → ℂ} (f : ℝ → ℂ) (hf : MemHS f) (hfg : f =ᵐ[MeasureTheory.volume] g) :
MemHS g := MemLp.ae_eq hfg hfConstruction of elements of the Hilbert space
lemma aeEqFun_mk_mem_iff (f : ℝ → ℂ) (hf : AEStronglyMeasurable f volume) :
AEEqFun.mk f hf ∈ HilbertSpace ↔ MemHS f := f:ℝ → ℂhf:AEStronglyMeasurable f volume⊢ AEEqFun.mk f hf ∈ HilbertSpace ↔ MemHS f
f:ℝ → ℂhf:AEStronglyMeasurable f volume⊢ MemLp (↑(AEEqFun.mk f hf)) 2 volume ↔ MemHS f
All goals completed! 🐙
Given a function f : ℝ → ℂ such that MemHS f is true via hf, then HilbertSpace.mk hf
is the element of the HilbertSpace defined by f.
def mk {f : ℝ → ℂ} (hf : MemHS f) : HilbertSpace :=
⟨AEEqFun.mk f hf.1, (aeEqFun_mk_mem_iff f hf.1).mpr hf⟩f:↥HilbertSpace⊢ AEEqFun.mk ↑↑f ⋯ ∈ HilbertSpace
f:↥HilbertSpacehf:↑f = AEEqFun.mk ↑↑f ⋯⊢ AEEqFun.mk ↑↑f ⋯ ∈ HilbertSpace
All goals completed! 🐙lemma mk_surjective (f : HilbertSpace) : ∃ (g : ℝ → ℂ), ∃ (hg : MemHS g), mk hg = f := f:↥HilbertSpace⊢ ∃ g, ∃ (hg : MemHS g), mk hg = f
f:↥HilbertSpace⊢ mk ⋯ = f
All goals completed! 🐙lemma coe_mk_ae {f : ℝ → ℂ} (hf : MemHS f) : (mk hf : ℝ → ℂ) =ᵐ[MeasureTheory.volume] f :=
AEEqFun.coeFn_mk f hf.1lemma inner_mk_mk {f g : ℝ → ℂ} {hf : MemHS f} {hg : MemHS g} :
inner ℂ (mk hf) (mk hg) = ∫ x : ℝ, starRingEnd ℂ (f x) * g x := f:ℝ → ℂg:ℝ → ℂhf:MemHS fhg:MemHS g⊢ ⟪mk hf, mk hg⟫_ℂ = ∫ (x : ℝ), (starRingEnd ℂ) (f x) * g x
f:ℝ → ℂg:ℝ → ℂhf:MemHS fhg:MemHS g⊢ (fun a => ⟪↑↑(mk hf) a, ↑↑(mk hg) a⟫_ℂ) =ᵐ[volume] fun a => (starRingEnd ℂ) (f a) * g a
filter_upwards [coe_mk_ae hf, coe_mk_ae hg] with _ f:ℝ → ℂg:ℝ → ℂhf✝:MemHS fhg:MemHS ga✝:ℝhf:↑↑(mk hf✝) a✝ = f a✝⊢ ↑↑(mk hg) a✝ = g a✝ → ⟪↑↑(mk hf✝) a✝, ↑↑(mk hg) a✝⟫_ℂ = (starRingEnd ℂ) (f a✝) * g a✝ f:ℝ → ℂg:ℝ → ℂhf✝:MemHS fhg✝:MemHS ga✝:ℝhf:↑↑(mk hf✝) a✝ = f a✝hg:↑↑(mk hg✝) a✝ = g a✝⊢ ⟪↑↑(mk hf✝) a✝, ↑↑(mk hg✝) a✝⟫_ℂ = (starRingEnd ℂ) (f a✝) * g a✝
All goals completed! 🐙@[simp]
lemma eLpNorm_mk {f : ℝ → ℂ} {hf : MemHS f} : eLpNorm (mk hf) 2 volume = eLpNorm f 2 volume :=
MeasureTheory.eLpNorm_congr_ae (coe_mk_ae hf)lemma mem_iff' {f : ℝ → ℂ} (hf : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume) :
MeasureTheory.AEEqFun.mk f hf ∈ HilbertSpace
↔ MeasureTheory.Integrable (fun x => ‖f x‖ ^ 2) := f:ℝ → ℂhf:AEStronglyMeasurable f volume⊢ AEEqFun.mk f hf ∈ HilbertSpace ↔ Integrable (fun x => ‖f x‖ ^ 2) volume
f:ℝ → ℂhf:AEStronglyMeasurable f volume⊢ AEStronglyMeasurable (↑(AEEqFun.mk f hf)) volume ∧ eLpNorm f 2 volume < ⊤ ↔ Integrable (fun x => ‖f x‖ ^ 2) volume
f:ℝ → ℂhf:AEStronglyMeasurable f volumeh1:AEStronglyMeasurable (↑(AEEqFun.mk f hf)) volume⊢ AEStronglyMeasurable (↑(AEEqFun.mk f hf)) volume ∧ eLpNorm f 2 volume < ⊤ ↔ Integrable (fun x => ‖f x‖ ^ 2) volume
f:ℝ → ℂhf:AEStronglyMeasurable f volumeh1:AEStronglyMeasurable (↑(AEEqFun.mk f hf)) volume⊢ ∫⁻ (a : ℝ), ‖f a‖ₑ ^ 2 < ⊤ ↔
AEStronglyMeasurable (fun x => ‖f x‖ ^ 2) volume ∧ HasFiniteIntegral (fun x => ‖f x‖ ^ 2) volume
f:ℝ → ℂhf:AEStronglyMeasurable f volumeh1:AEStronglyMeasurable (↑(AEEqFun.mk f hf)) volumeh0:AEStronglyMeasurable (fun x => ‖f x‖ ^ 2) volume⊢ ∫⁻ (a : ℝ), ‖f a‖ₑ ^ 2 < ⊤ ↔
AEStronglyMeasurable (fun x => ‖f x‖ ^ 2) volume ∧ HasFiniteIntegral (fun x => ‖f x‖ ^ 2) volume
All goals completed! 🐙lemma mk_add {f g : ℝ → ℂ} {hf : MemHS f} {hg : MemHS g} :
mk (memHS_add hf hg) = mk hf + mk hg := rfllemma mk_smul {f : ℝ → ℂ} {c : ℂ} {hf : MemHS f} :
mk (memHS_smul (c := c) hf) = c • mk hf := rfllemma mk_eq_iff {f g : ℝ → ℂ} {hf : MemHS f} {hg : MemHS g} :
mk hf = mk hg ↔ f =ᵐ[volume] g := f:ℝ → ℂg:ℝ → ℂhf:MemHS fhg:MemHS g⊢ mk hf = mk hg ↔ f =ᵐ[volume] g
All goals completed! 🐙lemma ext_iff {f g : HilbertSpace} :
f = g ↔ (f : ℝ → ℂ) =ᶠ[ae volume] (g : ℝ → ℂ) := f:↥HilbertSpaceg:↥HilbertSpace⊢ f = g ↔ ↑↑f =ᵐ[volume] ↑↑g
All goals completed! 🐙