From d3de12c7f4dc309da1ca1c1788bd733769511286 Mon Sep 17 00:00:00 2001 From: gloges Date: Sat, 21 Feb 2026 21:30:30 +0900 Subject: [PATCH 01/21] d-dim Hilbert space --- PhysLean.lean | 1 + .../DDimensions/SpaceDHilbertSpace/Basic.lean | 151 ++++++++++++++++++ 2 files changed, 152 insertions(+) create mode 100644 PhysLean/QuantumMechanics/DDimensions/SpaceDHilbertSpace/Basic.lean diff --git a/PhysLean.lean b/PhysLean.lean index 860eff1c2..b749b37b1 100644 --- a/PhysLean.lean +++ b/PhysLean.lean @@ -232,6 +232,7 @@ import PhysLean.QuantumMechanics.DDimensions.Operators.AngularMomentum import PhysLean.QuantumMechanics.DDimensions.Operators.Commutation import PhysLean.QuantumMechanics.DDimensions.Operators.Momentum import PhysLean.QuantumMechanics.DDimensions.Operators.Position +import PhysLean.QuantumMechanics.DDimensions.SpaceDHilbertSpace.Basic import PhysLean.QuantumMechanics.FiniteTarget.Basic import PhysLean.QuantumMechanics.FiniteTarget.HilbertSpace import PhysLean.QuantumMechanics.OneDimension.GeneralPotential.Basic diff --git a/PhysLean/QuantumMechanics/DDimensions/SpaceDHilbertSpace/Basic.lean b/PhysLean/QuantumMechanics/DDimensions/SpaceDHilbertSpace/Basic.lean new file mode 100644 index 000000000..e84b96f02 --- /dev/null +++ b/PhysLean/QuantumMechanics/DDimensions/SpaceDHilbertSpace/Basic.lean @@ -0,0 +1,151 @@ +/- +Copyright (c) 2026 Gregory J. Loges. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Gregory J. Loges +-/ +import Mathlib.Analysis.InnerProductSpace.Dual +import Mathlib.MeasureTheory.Function.L2Space +import PhysLean.SpaceAndTime.Space.Basic +/-! + +# Hilbert space for quantum mechanics on Space d + +-/ + +namespace QuantumMechanics + +noncomputable section + +/-- The Hilbert space for single-particle quantum mechanics on `Space d` is defined to be + `L²(Space d, ℂ)`, the space of almost-everywhere equal equivalence classes of square-integrable + functions from `Space d` to `ℂ`. -/ +abbrev SpaceDHilbertSpace (d : ℕ) := MeasureTheory.Lp (α := Space d) ℂ 2 + +namespace SpaceDHilbertSpace +open MeasureTheory +open InnerProductSpace + +/-- The anti-linear map from the Hilbert space to its dual. -/ +def toBra {d : ℕ} : SpaceDHilbertSpace d →ₛₗ[starRingEnd ℂ] (StrongDual ℂ (SpaceDHilbertSpace d)) := + toDual ℂ (SpaceDHilbertSpace d) + +@[simp] +lemma toBra_apply (f g : SpaceDHilbertSpace d) : toBra f g = ⟪f, g⟫_ℂ := rfl + +/-- The anti-linear map `toBra` taking a ket to its corresponding bra is surjective. -/ +lemma toBra_surjective : Function.Surjective (toBra (d := d)) := + (toDual ℂ (SpaceDHilbertSpace d)).surjective + +/-- The anti-linear map `toBra` taking a ket to its corresponding bra is injective. -/ +lemma toBra_injective : Function.Injective (toBra (d := d)) := by + intro f g h + simpa [toBra] using h + +/-! +## Member of the Hilbert space as a property +-/ + +/-- The proposition `MemHS f` for a function `f : Space d → ℂ` is defined + to be true if the function `f` can be lifted to the Hilbert space. -/ +def MemHS (f : Space d → ℂ) : Prop := MemLp f 2 + +lemma aeStronglyMeasurable_of_memHS {f : Space d → ℂ} (h : MemHS f) : AEStronglyMeasurable f := + MemLp.aestronglyMeasurable h + +/-- A function `f` satisfies `MemHS f` if and only if it is almost everywhere + strongly measurable and square integrable. -/ +lemma memHS_iff {f : Space d → ℂ} : MemHS f ↔ + AEStronglyMeasurable f ∧ Integrable (fun x ↦ ‖f x‖ ^ 2) := by + rw [MemHS, MemLp, and_congr_right] + intro h + rw [eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top + (NeZero.ne' 2).symm ENNReal.top_ne_ofNat.symm] + simp only [ENNReal.toReal_ofNat, ENNReal.rpow_ofNat] + have h' : AEStronglyMeasurable (fun x ↦ ‖f x‖ ^ 2) := + AEStronglyMeasurable.pow (AEStronglyMeasurable.norm h) 2 + simp [Integrable, h', HasFiniteIntegral] + +@[simp] +lemma zero_memHS : MemHS (d := d) 0 := by + rw [memHS_iff] + simp only [Pi.zero_apply, norm_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, + integrable_zero, and_true] + fun_prop + +@[simp] +lemma zero_fun_memHS : MemHS (fun _ : Space d ↦ (0 : ℂ)) := zero_memHS + +lemma memHS_add {f g : Space d → ℂ} (hf : MemHS f) (hg : MemHS g) : MemHS (f + g) := + MemLp.add hf hg + +lemma memHS_const_smul {f : Space d → ℂ} {c : ℂ} (hf : MemHS f) : MemHS (c • f) := + MemLp.const_smul hf c + +lemma memHS_of_ae {g : Space d → ℂ} (f : Space d → ℂ) (hf : MemHS f) (hfg : f =ᵐ[volume] g) : + MemHS g := MemLp.ae_eq hfg hf + +/-! +## Construction of elements of the Hilbert space +-/ + +lemma aeEqFun_mk_mem_iff (f : Space d → ℂ) (hf : AEStronglyMeasurable f volume) : + AEEqFun.mk f hf ∈ SpaceDHilbertSpace d ↔ MemHS f := by + rw [Lp.mem_Lp_iff_memLp] + exact memLp_congr_ae (AEEqFun.coeFn_mk f hf) + +/-- Given a function `f : Space d → ℂ` such that `MemHS f` is true via `hf`, + `SpaceDHilbertSpace.mk f` is the element of the Hilbert space defined by `f`. -/ +def mk {f : Space d → ℂ} (hf : MemHS f) : SpaceDHilbertSpace d := + ⟨AEEqFun.mk f hf.1, (aeEqFun_mk_mem_iff f hf.1).mpr hf⟩ + +lemma coe_hilbertSpace_memHS (f : SpaceDHilbertSpace d) : MemHS (f : Space d → ℂ) := by + rw [← aeEqFun_mk_mem_iff f (Lp.aestronglyMeasurable f)] + have hf : f = AEEqFun.mk f (Lp.aestronglyMeasurable f) := (AEEqFun.mk_coeFn _).symm + exact hf ▸ f.2 + +lemma mk_surjective (f : SpaceDHilbertSpace d) : + ∃ (g : Space d → ℂ), ∃ (hg : MemHS g), mk hg = f := by + use f, coe_hilbertSpace_memHS f + simp [mk] + +lemma coe_mk_ae {f : Space d → ℂ} (hf : MemHS f) : (mk hf) =ᵐ[volume] f := + AEEqFun.coeFn_mk f hf.1 + +lemma inner_mk_mk {f g : Space d → ℂ} (hf : MemHS f) (hg : MemHS g) : + ⟪mk hf, mk hg⟫_ℂ = ∫ x : Space d, starRingEnd ℂ (f x) * g x := by + apply integral_congr_ae + filter_upwards [coe_mk_ae hf, coe_mk_ae hg] with x hf hg + simp [hf, hg, mul_comm] + +@[simp] +lemma eLpNorm_mk {f : Space d → ℂ} {hf : MemHS f} : eLpNorm (mk hf) 2 = eLpNorm f 2 := + eLpNorm_congr_ae (coe_mk_ae hf) + +lemma mem_iff {f : Space d → ℂ} (hf : AEStronglyMeasurable f volume) : + AEEqFun.mk f hf ∈ SpaceDHilbertSpace d ↔ Integrable (fun x ↦ ‖f x‖ ^ 2) := by + rw [Lp.mem_Lp_iff_memLp, MemLp, eLpNorm_aeeqFun] + + have h1 := AEEqFun.aestronglyMeasurable (AEEqFun.mk f hf) + have h2 : AEStronglyMeasurable (fun x ↦ norm (f x) ^ 2) := + AEStronglyMeasurable.pow (continuous_norm.comp_aestronglyMeasurable hf) 2 + + simp only [h1, true_and, Integrable] + simp only [eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top (NeZero.ne' 2).symm + (ENNReal.top_ne_ofNat).symm, ENNReal.toReal_ofNat, ENNReal.rpow_ofNat] + simp [h2, HasFiniteIntegral] + +lemma mk_add {f g : Space d → ℂ} {hf : MemHS f} {hg : MemHS g} : + mk (memHS_add hf hg) = mk hf + mk hg := rfl + +lemma mk_const_smul {f : Space d → ℂ} {c : ℂ} {hf : MemHS f} : + mk (memHS_const_smul (c := c) hf) = c • mk hf := rfl + +lemma mk_eq_iff {f g : Space d → ℂ} {hf : MemHS f} {hg : MemHS g} : + mk hf = mk hg ↔ f =ᵐ[volume] g := by simp [mk] + +lemma ext_iff {f g : SpaceDHilbertSpace d} : + f = g ↔ (f : Space d → ℂ) =ᵐ[volume] (g : Space d → ℂ) := Lp.ext_iff + +end SpaceDHilbertSpace +end +end QuantumMechanics From 4941a2507b0d6c5d30b2d69ae7007b4419a98ab8 Mon Sep 17 00:00:00 2001 From: gloges Date: Sat, 21 Feb 2026 21:36:05 +0900 Subject: [PATCH 02/21] d-dim schwartz submodule --- PhysLean.lean | 1 + .../SpaceDHilbertSpace/SchwartzSubmodule.lean | 51 +++++++++++++++++++ 2 files changed, 52 insertions(+) create mode 100644 PhysLean/QuantumMechanics/DDimensions/SpaceDHilbertSpace/SchwartzSubmodule.lean diff --git a/PhysLean.lean b/PhysLean.lean index b749b37b1..e329bcf89 100644 --- a/PhysLean.lean +++ b/PhysLean.lean @@ -233,6 +233,7 @@ import PhysLean.QuantumMechanics.DDimensions.Operators.Commutation import PhysLean.QuantumMechanics.DDimensions.Operators.Momentum import PhysLean.QuantumMechanics.DDimensions.Operators.Position import PhysLean.QuantumMechanics.DDimensions.SpaceDHilbertSpace.Basic +import PhysLean.QuantumMechanics.DDimensions.SpaceDHilbertSpace.SchwartzSubmodule import PhysLean.QuantumMechanics.FiniteTarget.Basic import PhysLean.QuantumMechanics.FiniteTarget.HilbertSpace import PhysLean.QuantumMechanics.OneDimension.GeneralPotential.Basic diff --git a/PhysLean/QuantumMechanics/DDimensions/SpaceDHilbertSpace/SchwartzSubmodule.lean b/PhysLean/QuantumMechanics/DDimensions/SpaceDHilbertSpace/SchwartzSubmodule.lean new file mode 100644 index 000000000..5876dd376 --- /dev/null +++ b/PhysLean/QuantumMechanics/DDimensions/SpaceDHilbertSpace/SchwartzSubmodule.lean @@ -0,0 +1,51 @@ +/- +Copyright (c) 2026 Gregory J. Loges. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Gregory J. Loges +-/ +import Mathlib.Analysis.Distribution.SchwartzSpace.Basic +import PhysLean.QuantumMechanics.DDimensions.SpaceDHilbertSpace.Basic +/-! + +# Schwartz submodule of the Hilbert space + +-/ + +namespace QuantumMechanics +namespace SpaceDHilbertSpace + +noncomputable section + +open MeasureTheory +open InnerProductSpace +open SchwartzMap + +/-- The continuous linear map including Schwartz functions into `SpaceDHilbertSpace d`. -/ +def schwartzIncl {d : ℕ} : 𝓢(Space d, ℂ) →L[ℂ] SpaceDHilbertSpace d := toLpCLM ℂ (E := Space d) ℂ 2 + +lemma schwartzIncl_injective {d : ℕ} : + Function.Injective (schwartzIncl (d := d)) := injective_toLp (E := Space d) 2 + +lemma schwartzIncl_coe_ae {d : ℕ} (f : 𝓢(Space d, ℂ)) : f.1 =ᵐ[volume] (schwartzIncl f) := + (coeFn_toLp f 2).symm + +lemma schwartzIncl_inner {d : ℕ} (f g : 𝓢(Space d, ℂ)) : + ⟪schwartzIncl f, schwartzIncl g⟫_ℂ = ∫ x : Space d, starRingEnd ℂ (f x) * g x := by + apply integral_congr_ae + have hf := schwartzIncl_coe_ae f + have hg := schwartzIncl_coe_ae g + filter_upwards [hf, hg] with _ hf hg + rw [← hf, ← hg] + rw [RCLike.inner_apply, mul_comm] + rfl + +/-- The submodule of `SpaceDHilbertSpace d` consisting of Schwartz functions. -/ +abbrev schwartzSubmodule (d : ℕ) := (schwartzIncl (d := d)).range + +lemma schwartzSubmodule_dense {d : ℕ} : + Dense (schwartzSubmodule d : Set (SpaceDHilbertSpace d)) := + denseRange_toLpCLM ENNReal.top_ne_ofNat.symm + +end +end SpaceDHilbertSpace +end QuantumMechanics From bcfa19c6f8d8781ab140e94c6ce44981c0aabf00 Mon Sep 17 00:00:00 2001 From: gloges Date: Sat, 21 Feb 2026 21:36:37 +0900 Subject: [PATCH 03/21] init progress on unbounded ops --- PhysLean.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/PhysLean.lean b/PhysLean.lean index e329bcf89..50c9d274c 100644 --- a/PhysLean.lean +++ b/PhysLean.lean @@ -232,6 +232,7 @@ import PhysLean.QuantumMechanics.DDimensions.Operators.AngularMomentum import PhysLean.QuantumMechanics.DDimensions.Operators.Commutation import PhysLean.QuantumMechanics.DDimensions.Operators.Momentum import PhysLean.QuantumMechanics.DDimensions.Operators.Position +import PhysLean.QuantumMechanics.DDimensions.Operators.Unbounded import PhysLean.QuantumMechanics.DDimensions.SpaceDHilbertSpace.Basic import PhysLean.QuantumMechanics.DDimensions.SpaceDHilbertSpace.SchwartzSubmodule import PhysLean.QuantumMechanics.FiniteTarget.Basic From 258b92528c16a3a095f8faeafbe25e5c72358d9e Mon Sep 17 00:00:00 2001 From: gloges Date: Sat, 21 Feb 2026 21:37:01 +0900 Subject: [PATCH 04/21] init progress on unbounded ops --- .../DDimensions/Operators/Unbounded.lean | 207 ++++++++++++++++++ 1 file changed, 207 insertions(+) create mode 100644 PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean diff --git a/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean b/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean new file mode 100644 index 000000000..7846103ef --- /dev/null +++ b/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean @@ -0,0 +1,207 @@ +/- +Copyright (c) 2026 Gregory J. Loges. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Gregory J. Loges +-/ +import Mathlib.Analysis.InnerProductSpace.LinearPMap +import PhysLean.QuantumMechanics.DDimensions.SpaceDHilbertSpace.SchwartzSubmodule +/-! + +# Unbounded operators + +-/ + +namespace QuantumMechanics + +noncomputable section + +open LinearPMap + +-- Nothing here uses any specific properties of this particular Hilbert space +abbrev hilbSp d := SpaceDHilbertSpace d + +/-- An `UnboundedOperator` is a linear map from a submodule of the Hilbert space + to the Hilbert space, assumed to be both densely defined and closable. -/ +@[ext] +structure UnboundedOperator (d : ℕ) where + /-- The LinearPMap defining the unbounded operator. -/ + toLinearPMap : LinearPMap ℂ (hilbSp d) (hilbSp d) + /-- The domain of the unbounded operator is dense in the Hilbert space. -/ + dense_domain : Dense (toLinearPMap.domain : Set (hilbSp d)) + /-- The unbounded operator is closable. -/ + is_closable : toLinearPMap.IsClosable + +namespace UnboundedOperator + +variable {d : ℕ} (U : UnboundedOperator d) + +/-- Domain of `UnboundedOperator`. -/ +def domain : Submodule ℂ (hilbSp d) := U.toLinearPMap.domain + +/-- `UnboundedOperator` as a function. -/ +@[coe] +def toFun : U.domain → (hilbSp d) := U.toLinearPMap.toFun + +instance : CoeFun (UnboundedOperator d) + (fun U : UnboundedOperator d ↦ U.domain → (hilbSp d)) := ⟨toFun⟩ + +@[simp] +lemma toFun_eq_coe (x : U.domain) : U.toFun x = U.toLinearPMap.toFun x := rfl + +/-! +## Construction of unbounded operators +-/ + +variable + {E : Submodule ℂ (hilbSp d)} + {hE : Dense (E : Set (hilbSp d))} + +/-- An `UnboundedOperator` constructed from a symmetric linear map on a dense submodule `E`. -/ +def ofSymmetric (f : E →ₗ[ℂ] E) (hf : f.IsSymmetric) : UnboundedOperator d where + toLinearPMap := LinearPMap.mk E (E.subtype ∘ₗ f) + dense_domain := hE + is_closable := by + -- TODO: symmetric ∧ dense ⇒ closable + unfold Dense at hE + unfold LinearMap.IsSymmetric at hf + sorry + +@[simp] +lemma ofSymmetric_apply {f : E →ₗ[ℂ] E} {hf : f.IsSymmetric} (ψ : E) : + (ofSymmetric (hE := hE) f hf).toLinearPMap ψ = E.subtypeL (f ψ) := rfl + +/-! +## Closure +-/ + +/-- The closure of an unbounded operator. -/ +def closure : UnboundedOperator d where + toLinearPMap := U.toLinearPMap.closure + dense_domain := by + refine Dense.mono ?_ U.dense_domain + exact HasCore.le_domain (closureHasCore U.toLinearPMap) + is_closable := IsClosed.isClosable (IsClosable.closure_isClosed U.is_closable) + +lemma closure_toLinearPMap : U.closure.toLinearPMap = U.toLinearPMap.closure := rfl + +def IsClosed : Prop := U.toLinearPMap.IsClosed + +lemma closure_isClosed : U.closure.IsClosed := IsClosable.closure_isClosed U.is_closable + +/-! +## Adjoints +-/ + +/-- The adjoint of an unbounded operator, denoted as `U†`. -/ +def adjoint : UnboundedOperator d where + toLinearPMap := U.toLinearPMap.adjoint + dense_domain := by sorry + is_closable := IsClosed.isClosable (adjoint_isClosed U.dense_domain) + +@[inherit_doc] +scoped postfix:1024 "†" => UnboundedOperator.adjoint + +instance instStar : Star (UnboundedOperator d) where + star := fun U ↦ U.adjoint + +lemma adjoint_toLinearPMap : U†.toLinearPMap = U.toLinearPMap† := rfl + +lemma isSelfAdjoint_def : IsSelfAdjoint U ↔ U† = U := Iff.rfl + +lemma isSelfAdjoint_iff : IsSelfAdjoint U ↔ IsSelfAdjoint U.toLinearPMap := by + rw [isSelfAdjoint_def, LinearPMap.isSelfAdjoint_def] + constructor <;> intro h + · rw [← adjoint_toLinearPMap, h] + · rwa [UnboundedOperator.ext_iff, adjoint_toLinearPMap] + +lemma adjoint_isClosed : (U†).IsClosed := LinearPMap.adjoint_isClosed U.dense_domain + +/- +TODO: Rework below using `PiLp 2` (see [https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/InnerProductSpace/PiL2.html]) +so that `hilbSp × hilbSp` has the structure of an inner product space. +-/ + +abbrev hilbSp2 (d : ℕ) := hilbSp d × hilbSp d + +def inner2 (f g : hilbSp2 d) : ℂ := inner ℂ f.1 g.1 + inner ℂ f.2 g.2 + +lemma closure_adjoint_eq_adjoint : U.closure† = U† := by + -- Reduce to statement about graphs using density and closability assumptions + apply UnboundedOperator.ext + apply LinearPMap.eq_of_eq_graph + rw [adjoint_toLinearPMap, adjoint_graph_eq_graph_adjoint U.closure.dense_domain] + rw [adjoint_toLinearPMap, adjoint_graph_eq_graph_adjoint U.dense_domain] + rw [closure_toLinearPMap, ← IsClosable.graph_closure_eq_closure_graph U.is_closable] + + -- Remains to show `(graph.closure)^⟂ = graph^⟂`, which is exactly `Submodule.orthogonal_closure`. + -- Need to "translate" to orthogonal complements and use inner product structure on `hilbSp2`. + sorry + +lemma adjoint_adjoint_eq_closure : U†† = U.closure := by + -- Reduce to statement about graphs using density and closability assumptions + apply UnboundedOperator.ext + apply LinearPMap.eq_of_eq_graph + rw [adjoint_toLinearPMap, adjoint_graph_eq_graph_adjoint U†.dense_domain] + rw [adjoint_toLinearPMap, adjoint_graph_eq_graph_adjoint U.dense_domain] + rw [closure_toLinearPMap, ← IsClosable.graph_closure_eq_closure_graph U.is_closable] + + ext ψUψ + simp only [Submodule.mem_adjoint_iff] + + -- Flip the sign of either `a` or `b` (which are general elements of `hilbSp` anyways) + -- and package conditions into statements of orthogonality in `hilbSp × hilbSp` + trans ∀ (f : hilbSp2 d), (∀ g ∈ U.toLinearPMap.graph, inner2 f g = 0) → inner2 f ψUψ = 0 + · constructor <;> intro h + · intro f h1 + have h2 := h (-f.2) f.1 + simp only [inner_neg_left, sub_neg_eq_add] at h2 + apply h2 + intro a b hab + rw [sub_eq_zero] + nth_rw 1 [← InnerProductSpace.conj_inner_symm] + nth_rw 2 [← InnerProductSpace.conj_inner_symm] + apply RingHom.congr_arg + rw [inner_neg_left, neg_eq_iff_add_eq_zero, add_comm] + exact h1 (a, b) hab + · intro a b h1 + rw [sub_eq_add_neg, ← inner_neg_left] + apply h (b, -a) + intro g hg + unfold inner2 + rw [inner_neg_left, add_neg_eq_zero] + nth_rw 1 [← InnerProductSpace.conj_inner_symm] + nth_rw 2 [← InnerProductSpace.conj_inner_symm] + apply RingHom.congr_arg + apply Eq.symm + rw [← sub_eq_zero] + exact h1 g.1 g.2 hg + + -- Remains to show that `(graph^⟂)^⟂ = graph.topologicalClosure`, + -- which is exactly `Submodule.orthogonal_orthogonal_eq_closure`. + -- Need to "translate" to orthogonal complements and use inner product structure on `hilbSp2`. + sorry + +/-! +## Generalized eigenvectors +-/ + +/-- A map `F : D(U) →L[ℂ] ℂ` is a generalized eigenvector of an unbounded operator `U` + if there is an eigenvalue `c` such that for all `ψ ∈ D(U)`, `F (U ψ) = c ⬝ F ψ`. -/ +def IsGeneralizedEigenvector (F : U.domain →L[ℂ] ℂ) (c : ℂ) : Prop := + ∀ ψ : U.domain, ∃ ψ' : U.domain, ψ' = U ψ ∧ F ψ' = c • F ψ + +lemma isGeneralizedEigenvector_ofSymmetric_iff + {f : E →ₗ[ℂ] E} {hf : f.IsSymmetric} (F : E →L[ℂ] ℂ) (c : ℂ) : + IsGeneralizedEigenvector (ofSymmetric (hE := hE) f hf) F c ↔ ∀ ψ : E, F (f ψ) = c • F ψ := by + constructor <;> intro h ψ + · obtain ⟨ψ', hψ', hψ''⟩ := h ψ + apply SetLike.coe_eq_coe.mp at hψ' + subst hψ' + exact hψ'' + · use f ψ + exact ⟨by simp, h ψ⟩ + +end UnboundedOperator + +end +end QuantumMechanics From 62454e461612231f97c377fad3731462feb3ef08 Mon Sep 17 00:00:00 2001 From: gloges Date: Sun, 22 Feb 2026 22:10:27 +0900 Subject: [PATCH 05/21] submodule lemmas --- .../DDimensions/Operators/Unbounded.lean | 142 ++++++++++++------ 1 file changed, 98 insertions(+), 44 deletions(-) diff --git a/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean b/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean index 7846103ef..79a6d9d68 100644 --- a/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean +++ b/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean @@ -116,14 +116,96 @@ lemma isSelfAdjoint_iff : IsSelfAdjoint U ↔ IsSelfAdjoint U.toLinearPMap := by lemma adjoint_isClosed : (U†).IsClosed := LinearPMap.adjoint_isClosed U.dense_domain -/- -TODO: Rework below using `PiLp 2` (see [https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/InnerProductSpace/PiL2.html]) -so that `hilbSp × hilbSp` has the structure of an inner product space. --/ +/-- `hilbSp × hilbSp` with inner product `⟪(f0, f1), (g0, g1)⟫ ≔ ⟪f0, g0⟫ + ⟪f1, g1⟫` + and induced norm `‖(f0, f1)‖² = ‖f0‖² + ‖f1‖²` (by default `H × H` is given the norm + `‖(f0, f1)‖ = max { ‖f0‖, ‖f1‖ }`) -/ +abbrev hilbSp2 (d : ℕ) := WithLp 2 (hilbSp d × hilbSp d) + +def submoduleToLp (E : Submodule ℂ (hilbSp d × hilbSp d)) : Submodule ℂ (hilbSp2 d) where + carrier := {x | x.ofLp ∈ E} + add_mem' := by + intro a b ha hb + exact Submodule.add_mem E ha hb + zero_mem' := Submodule.zero_mem E + smul_mem' := by + intro c x hx + exact Submodule.smul_mem E c hx + +lemma submoduleToLp_closure (E : Submodule ℂ (hilbSp d × hilbSp d)) : + (submoduleToLp E.closure) = (submoduleToLp E).topologicalClosure := by + rw [Submodule.ext_iff] + simp [← Submodule.mem_closure_iff] -- Is this needed? + intro x + -- TODO: `toLp E.closure = (toLp E).closure` + -- This is nontrivial: + -- In `submoduleToLp E.closure` the closure is wrt the sup norm (by default `H × H` is equipped + -- with a norm defined as the supremum of the norms of their components). + -- In `(submoduleToLp E).closure` the closure is wrt the L² norm introduced above. + -- Need to use that `Lp` norms induce the same topology in two dimensions (two copies of `H`). + sorry -abbrev hilbSp2 (d : ℕ) := hilbSp d × hilbSp d +lemma mem_submodule_iff_mem_submoduleToLp (E : Submodule ℂ (hilbSp d × hilbSp d)) : + ∀ f, f ∈ E ↔ (WithLp.toLp 2 f) ∈ submoduleToLp E := fun _ => Eq.to_iff rfl -def inner2 (f g : hilbSp2 d) : ℂ := inner ℂ f.1 g.1 + inner ℂ f.2 g.2 +lemma mem_submodule_closure_iff_mem_submoduleToLp_closure (E : Submodule ℂ (hilbSp d × hilbSp d)) : + ∀ f, f ∈ E.topologicalClosure ↔ (WithLp.toLp 2 f) ∈ (submoduleToLp E).topologicalClosure := by + intro f + rw [← submoduleToLp_closure] + rfl + +lemma mem_submodule_adjoint_iff_mem_submoduleToLp_orthogonal + (E : Submodule ℂ (hilbSp d × hilbSp d)) : + ∀ f, f ∈ E.adjoint ↔ WithLp.toLp 2 (f.2, -f.1) ∈ (submoduleToLp E)ᗮ := by + intro f + constructor <;> intro h + · rw [Submodule.mem_orthogonal] + intro u hu + rw [Submodule.mem_adjoint_iff] at h + have h' : inner ℂ u.snd f.1 = inner ℂ u.fst f.2 := by + rw [← sub_eq_zero] + exact h u.fst u.snd hu + simp [h'] + · rw [Submodule.mem_adjoint_iff] + intro a b hab + rw [Submodule.mem_orthogonal] at h + have hab' : (WithLp.toLp 2 (a, b)) ∈ submoduleToLp E := by + exact (mem_submodule_iff_mem_submoduleToLp E (a, b)).mp hab + have h' : inner ℂ a f.2 = inner ℂ b f.1 := by + rw [← sub_eq_zero, sub_eq_add_neg, ← inner_neg_right] + exact h (WithLp.toLp 2 (a, b)) hab' + simp [h'] + +lemma mem_submodule_adjoint_adjoint_iff_mem_submoduleToLp_orthogonal_orthogonal + (E: Submodule ℂ (hilbSp d × hilbSp d)): + ∀ f, f ∈ E.adjoint.adjoint ↔ WithLp.toLp 2 f ∈ (submoduleToLp E)ᗮᗮ := by + intro f + simp only [Submodule.mem_adjoint_iff] + trans ∀ v, (∀ w ∈ submoduleToLp E, inner ℂ w v = 0) → inner ℂ v (WithLp.toLp 2 f) = 0 + · constructor <;> intro h + · intro v hw + have h' := h (-v.snd) v.fst + rw [inner_neg_left, sub_neg_eq_add] at h' + apply h' + intro a b hab + rw [inner_neg_right, neg_sub_left, neg_eq_zero] + exact hw (WithLp.toLp 2 (a, b)) ((mem_submodule_iff_mem_submoduleToLp E (a, b)).mp hab) + · intro a b h' + rw [sub_eq_add_neg, ← inner_neg_left] + apply h (WithLp.toLp 2 (b, -a)) + intro w hw + have hw' := h' w.fst w.snd hw + rw [sub_eq_zero] at hw' + simp [hw'] + simp only [← Submodule.mem_orthogonal] + +lemma mem_submodule_closure_adjoint_iff_mem_submoduleToLp_closure_orthogonal + (E : Submodule ℂ (hilbSp d × hilbSp d)) : + ∀ f, f ∈ E.closure.adjoint ↔ WithLp.toLp 2 (f.2, -f.1) ∈ (submoduleToLp E).closureᗮ := by + intro f + trans (WithLp.toLp 2 (f.2, -f.1)) ∈ (submoduleToLp E.closure)ᗮ + · apply mem_submodule_adjoint_iff_mem_submoduleToLp_orthogonal E.closure f + rw [submoduleToLp_closure] + simp [← ClosedSubmodule.mem_toSubmodule_iff] lemma closure_adjoint_eq_adjoint : U.closure† = U† := by -- Reduce to statement about graphs using density and closability assumptions @@ -133,9 +215,11 @@ lemma closure_adjoint_eq_adjoint : U.closure† = U† := by rw [adjoint_toLinearPMap, adjoint_graph_eq_graph_adjoint U.dense_domain] rw [closure_toLinearPMap, ← IsClosable.graph_closure_eq_closure_graph U.is_closable] - -- Remains to show `(graph.closure)^⟂ = graph^⟂`, which is exactly `Submodule.orthogonal_closure`. - -- Need to "translate" to orthogonal complements and use inner product structure on `hilbSp2`. - sorry + ext f + trans WithLp.toLp 2 (f.2, -f.1) ∈ (submoduleToLp U.toLinearPMap.graph).topologicalClosureᗮ + · exact mem_submodule_closure_adjoint_iff_mem_submoduleToLp_closure_orthogonal _ _ + rw [Submodule.orthogonal_closure] + exact Iff.symm (mem_submodule_adjoint_iff_mem_submoduleToLp_orthogonal _ _) lemma adjoint_adjoint_eq_closure : U†† = U.closure := by -- Reduce to statement about graphs using density and closability assumptions @@ -145,41 +229,11 @@ lemma adjoint_adjoint_eq_closure : U†† = U.closure := by rw [adjoint_toLinearPMap, adjoint_graph_eq_graph_adjoint U.dense_domain] rw [closure_toLinearPMap, ← IsClosable.graph_closure_eq_closure_graph U.is_closable] - ext ψUψ - simp only [Submodule.mem_adjoint_iff] - - -- Flip the sign of either `a` or `b` (which are general elements of `hilbSp` anyways) - -- and package conditions into statements of orthogonality in `hilbSp × hilbSp` - trans ∀ (f : hilbSp2 d), (∀ g ∈ U.toLinearPMap.graph, inner2 f g = 0) → inner2 f ψUψ = 0 - · constructor <;> intro h - · intro f h1 - have h2 := h (-f.2) f.1 - simp only [inner_neg_left, sub_neg_eq_add] at h2 - apply h2 - intro a b hab - rw [sub_eq_zero] - nth_rw 1 [← InnerProductSpace.conj_inner_symm] - nth_rw 2 [← InnerProductSpace.conj_inner_symm] - apply RingHom.congr_arg - rw [inner_neg_left, neg_eq_iff_add_eq_zero, add_comm] - exact h1 (a, b) hab - · intro a b h1 - rw [sub_eq_add_neg, ← inner_neg_left] - apply h (b, -a) - intro g hg - unfold inner2 - rw [inner_neg_left, add_neg_eq_zero] - nth_rw 1 [← InnerProductSpace.conj_inner_symm] - nth_rw 2 [← InnerProductSpace.conj_inner_symm] - apply RingHom.congr_arg - apply Eq.symm - rw [← sub_eq_zero] - exact h1 g.1 g.2 hg - - -- Remains to show that `(graph^⟂)^⟂ = graph.topologicalClosure`, - -- which is exactly `Submodule.orthogonal_orthogonal_eq_closure`. - -- Need to "translate" to orthogonal complements and use inner product structure on `hilbSp2`. - sorry + ext f + trans WithLp.toLp 2 f ∈ (submoduleToLp U.toLinearPMap.graph)ᗮᗮ + · exact mem_submodule_adjoint_adjoint_iff_mem_submoduleToLp_orthogonal_orthogonal _ _ + rw [Submodule.orthogonal_orthogonal_eq_closure] + rw [mem_submodule_closure_iff_mem_submoduleToLp_closure] /-! ## Generalized eigenvectors From f0d6bc7c1328fe082400ac2888639cbe8d39c627 Mon Sep 17 00:00:00 2001 From: gloges Date: Sun, 22 Feb 2026 22:51:07 +0900 Subject: [PATCH 06/21] abstract away Hilbert space --- .../DDimensions/Operators/Unbounded.lean | 107 ++++++++---------- 1 file changed, 49 insertions(+), 58 deletions(-) diff --git a/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean b/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean index 79a6d9d68..536b8c470 100644 --- a/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean +++ b/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean @@ -17,33 +17,35 @@ noncomputable section open LinearPMap --- Nothing here uses any specific properties of this particular Hilbert space -abbrev hilbSp d := SpaceDHilbertSpace d - /-- An `UnboundedOperator` is a linear map from a submodule of the Hilbert space to the Hilbert space, assumed to be both densely defined and closable. -/ @[ext] -structure UnboundedOperator (d : ℕ) where +structure UnboundedOperator + (HS : Type) [NormedAddCommGroup HS] [InnerProductSpace ℂ HS] [CompleteSpace HS] where /-- The LinearPMap defining the unbounded operator. -/ - toLinearPMap : LinearPMap ℂ (hilbSp d) (hilbSp d) + toLinearPMap : LinearPMap ℂ HS HS /-- The domain of the unbounded operator is dense in the Hilbert space. -/ - dense_domain : Dense (toLinearPMap.domain : Set (hilbSp d)) + dense_domain : Dense (toLinearPMap.domain : Set HS) /-- The unbounded operator is closable. -/ is_closable : toLinearPMap.IsClosable namespace UnboundedOperator -variable {d : ℕ} (U : UnboundedOperator d) +variable + {HS : Type} [NormedAddCommGroup HS] [InnerProductSpace ℂ HS] [CompleteSpace HS] + (U : UnboundedOperator HS) + {E : Submodule ℂ HS} {hE : Dense (E : Set HS)} + (F : Submodule ℂ (HS × HS)) /-- Domain of `UnboundedOperator`. -/ -def domain : Submodule ℂ (hilbSp d) := U.toLinearPMap.domain +def domain : Submodule ℂ HS := U.toLinearPMap.domain /-- `UnboundedOperator` as a function. -/ @[coe] -def toFun : U.domain → (hilbSp d) := U.toLinearPMap.toFun +def toFun : U.domain → HS := U.toLinearPMap.toFun -instance : CoeFun (UnboundedOperator d) - (fun U : UnboundedOperator d ↦ U.domain → (hilbSp d)) := ⟨toFun⟩ +instance : CoeFun (UnboundedOperator HS) + (fun U : UnboundedOperator HS ↦ U.domain → HS) := ⟨toFun⟩ @[simp] lemma toFun_eq_coe (x : U.domain) : U.toFun x = U.toLinearPMap.toFun x := rfl @@ -52,12 +54,8 @@ lemma toFun_eq_coe (x : U.domain) : U.toFun x = U.toLinearPMap.toFun x := rfl ## Construction of unbounded operators -/ -variable - {E : Submodule ℂ (hilbSp d)} - {hE : Dense (E : Set (hilbSp d))} - /-- An `UnboundedOperator` constructed from a symmetric linear map on a dense submodule `E`. -/ -def ofSymmetric (f : E →ₗ[ℂ] E) (hf : f.IsSymmetric) : UnboundedOperator d where +def ofSymmetric (f : E →ₗ[ℂ] E) (hf : f.IsSymmetric) : UnboundedOperator HS where toLinearPMap := LinearPMap.mk E (E.subtype ∘ₗ f) dense_domain := hE is_closable := by @@ -75,11 +73,9 @@ lemma ofSymmetric_apply {f : E →ₗ[ℂ] E} {hf : f.IsSymmetric} (ψ : E) : -/ /-- The closure of an unbounded operator. -/ -def closure : UnboundedOperator d where +def closure : UnboundedOperator HS where toLinearPMap := U.toLinearPMap.closure - dense_domain := by - refine Dense.mono ?_ U.dense_domain - exact HasCore.le_domain (closureHasCore U.toLinearPMap) + dense_domain := Dense.mono (HasCore.le_domain (closureHasCore U.toLinearPMap)) U.dense_domain is_closable := IsClosed.isClosable (IsClosable.closure_isClosed U.is_closable) lemma closure_toLinearPMap : U.closure.toLinearPMap = U.toLinearPMap.closure := rfl @@ -93,15 +89,17 @@ lemma closure_isClosed : U.closure.IsClosed := IsClosable.closure_isClosed U.is_ -/ /-- The adjoint of an unbounded operator, denoted as `U†`. -/ -def adjoint : UnboundedOperator d where +def adjoint : UnboundedOperator HS where toLinearPMap := U.toLinearPMap.adjoint - dense_domain := by sorry + dense_domain := by + -- TODO: `U` is closable ⇒ `U†` is densely defined + sorry is_closable := IsClosed.isClosable (adjoint_isClosed U.dense_domain) @[inherit_doc] scoped postfix:1024 "†" => UnboundedOperator.adjoint -instance instStar : Star (UnboundedOperator d) where +instance instStar : Star (UnboundedOperator HS) where star := fun U ↦ U.adjoint lemma adjoint_toLinearPMap : U†.toLinearPMap = U.toLinearPMap† := rfl @@ -116,46 +114,42 @@ lemma isSelfAdjoint_iff : IsSelfAdjoint U ↔ IsSelfAdjoint U.toLinearPMap := by lemma adjoint_isClosed : (U†).IsClosed := LinearPMap.adjoint_isClosed U.dense_domain -/-- `hilbSp × hilbSp` with inner product `⟪(f0, f1), (g0, g1)⟫ ≔ ⟪f0, g0⟫ + ⟪f1, g1⟫` - and induced norm `‖(f0, f1)‖² = ‖f0‖² + ‖f1‖²` (by default `H × H` is given the norm - `‖(f0, f1)‖ = max { ‖f0‖, ‖f1‖ }`) -/ -abbrev hilbSp2 (d : ℕ) := WithLp 2 (hilbSp d × hilbSp d) - -def submoduleToLp (E : Submodule ℂ (hilbSp d × hilbSp d)) : Submodule ℂ (hilbSp2 d) where - carrier := {x | x.ofLp ∈ E} +def submoduleToLp : Submodule ℂ (WithLp 2 (HS × HS)) where + carrier := {x | x.ofLp ∈ F} add_mem' := by intro a b ha hb - exact Submodule.add_mem E ha hb - zero_mem' := Submodule.zero_mem E + exact Submodule.add_mem F ha hb + zero_mem' := Submodule.zero_mem F smul_mem' := by intro c x hx - exact Submodule.smul_mem E c hx + exact Submodule.smul_mem F c hx -lemma submoduleToLp_closure (E : Submodule ℂ (hilbSp d × hilbSp d)) : - (submoduleToLp E.closure) = (submoduleToLp E).topologicalClosure := by +lemma submoduleToLp_closure : + (submoduleToLp F.closure) = (submoduleToLp F).topologicalClosure := by rw [Submodule.ext_iff] simp [← Submodule.mem_closure_iff] -- Is this needed? intro x - -- TODO: `toLp E.closure = (toLp E).closure` + -- TODO: `toLp F.closure = (toLp F).closure` -- This is nontrivial: - -- In `submoduleToLp E.closure` the closure is wrt the sup norm (by default `H × H` is equipped + -- In `submoduleToLp F.closure` the closure is wrt the sup norm (by default `H × H` is equipped -- with a norm defined as the supremum of the norms of their components). - -- In `(submoduleToLp E).closure` the closure is wrt the L² norm introduced above. + -- In `(submoduleToLp F).closure` the closure is wrt the L² norm introduced above. -- Need to use that `Lp` norms induce the same topology in two dimensions (two copies of `H`). sorry -lemma mem_submodule_iff_mem_submoduleToLp (E : Submodule ℂ (hilbSp d × hilbSp d)) : - ∀ f, f ∈ E ↔ (WithLp.toLp 2 f) ∈ submoduleToLp E := fun _ => Eq.to_iff rfl +omit [CompleteSpace HS] in +lemma mem_submodule_iff_mem_submoduleToLp : + ∀ f, f ∈ F ↔ (WithLp.toLp 2 f) ∈ submoduleToLp F := fun _ => Eq.to_iff rfl -lemma mem_submodule_closure_iff_mem_submoduleToLp_closure (E : Submodule ℂ (hilbSp d × hilbSp d)) : - ∀ f, f ∈ E.topologicalClosure ↔ (WithLp.toLp 2 f) ∈ (submoduleToLp E).topologicalClosure := by +lemma mem_submodule_closure_iff_mem_submoduleToLp_closure : + ∀ f, f ∈ F.topologicalClosure ↔ (WithLp.toLp 2 f) ∈ (submoduleToLp F).topologicalClosure := by intro f rw [← submoduleToLp_closure] rfl -lemma mem_submodule_adjoint_iff_mem_submoduleToLp_orthogonal - (E : Submodule ℂ (hilbSp d × hilbSp d)) : - ∀ f, f ∈ E.adjoint ↔ WithLp.toLp 2 (f.2, -f.1) ∈ (submoduleToLp E)ᗮ := by +omit [CompleteSpace HS] in +lemma mem_submodule_adjoint_iff_mem_submoduleToLp_orthogonal : + ∀ f, f ∈ F.adjoint ↔ WithLp.toLp 2 (f.2, -f.1) ∈ (submoduleToLp F)ᗮ := by intro f constructor <;> intro h · rw [Submodule.mem_orthogonal] @@ -168,19 +162,18 @@ lemma mem_submodule_adjoint_iff_mem_submoduleToLp_orthogonal · rw [Submodule.mem_adjoint_iff] intro a b hab rw [Submodule.mem_orthogonal] at h - have hab' : (WithLp.toLp 2 (a, b)) ∈ submoduleToLp E := by - exact (mem_submodule_iff_mem_submoduleToLp E (a, b)).mp hab + have hab' := (mem_submodule_iff_mem_submoduleToLp F (a, b)).mp hab have h' : inner ℂ a f.2 = inner ℂ b f.1 := by rw [← sub_eq_zero, sub_eq_add_neg, ← inner_neg_right] exact h (WithLp.toLp 2 (a, b)) hab' simp [h'] -lemma mem_submodule_adjoint_adjoint_iff_mem_submoduleToLp_orthogonal_orthogonal - (E: Submodule ℂ (hilbSp d × hilbSp d)): - ∀ f, f ∈ E.adjoint.adjoint ↔ WithLp.toLp 2 f ∈ (submoduleToLp E)ᗮᗮ := by +omit [CompleteSpace HS] in +lemma mem_submodule_adjoint_adjoint_iff_mem_submoduleToLp_orthogonal_orthogonal : + ∀ f, f ∈ F.adjoint.adjoint ↔ WithLp.toLp 2 f ∈ (submoduleToLp F)ᗮᗮ := by intro f simp only [Submodule.mem_adjoint_iff] - trans ∀ v, (∀ w ∈ submoduleToLp E, inner ℂ w v = 0) → inner ℂ v (WithLp.toLp 2 f) = 0 + trans ∀ v, (∀ w ∈ submoduleToLp F, inner ℂ w v = 0) → inner ℂ v (WithLp.toLp 2 f) = 0 · constructor <;> intro h · intro v hw have h' := h (-v.snd) v.fst @@ -188,7 +181,7 @@ lemma mem_submodule_adjoint_adjoint_iff_mem_submoduleToLp_orthogonal_orthogonal apply h' intro a b hab rw [inner_neg_right, neg_sub_left, neg_eq_zero] - exact hw (WithLp.toLp 2 (a, b)) ((mem_submodule_iff_mem_submoduleToLp E (a, b)).mp hab) + exact hw (WithLp.toLp 2 (a, b)) ((mem_submodule_iff_mem_submoduleToLp F (a, b)).mp hab) · intro a b h' rw [sub_eq_add_neg, ← inner_neg_left] apply h (WithLp.toLp 2 (b, -a)) @@ -198,12 +191,11 @@ lemma mem_submodule_adjoint_adjoint_iff_mem_submoduleToLp_orthogonal_orthogonal simp [hw'] simp only [← Submodule.mem_orthogonal] -lemma mem_submodule_closure_adjoint_iff_mem_submoduleToLp_closure_orthogonal - (E : Submodule ℂ (hilbSp d × hilbSp d)) : - ∀ f, f ∈ E.closure.adjoint ↔ WithLp.toLp 2 (f.2, -f.1) ∈ (submoduleToLp E).closureᗮ := by +lemma mem_submodule_closure_adjoint_iff_mem_submoduleToLp_closure_orthogonal : + ∀ f, f ∈ F.closure.adjoint ↔ WithLp.toLp 2 (f.2, -f.1) ∈ (submoduleToLp F).closureᗮ := by intro f - trans (WithLp.toLp 2 (f.2, -f.1)) ∈ (submoduleToLp E.closure)ᗮ - · apply mem_submodule_adjoint_iff_mem_submoduleToLp_orthogonal E.closure f + trans (WithLp.toLp 2 (f.2, -f.1)) ∈ (submoduleToLp F.closure)ᗮ + · apply mem_submodule_adjoint_iff_mem_submoduleToLp_orthogonal F.closure f rw [submoduleToLp_closure] simp [← ClosedSubmodule.mem_toSubmodule_iff] @@ -256,6 +248,5 @@ lemma isGeneralizedEigenvector_ofSymmetric_iff exact ⟨by simp, h ψ⟩ end UnboundedOperator - end end QuantumMechanics From 377e3139b41eb8a3a9409760b7fd38bc56edfed4 Mon Sep 17 00:00:00 2001 From: gloges Date: Sun, 22 Feb 2026 23:49:41 +0900 Subject: [PATCH 07/21] linter fixes --- .../DDimensions/Operators/Unbounded.lean | 11 ++++++----- .../DDimensions/SpaceDHilbertSpace/Basic.lean | 6 +++--- .../SpaceDHilbertSpace/SchwartzSubmodule.lean | 4 ++-- 3 files changed, 11 insertions(+), 10 deletions(-) diff --git a/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean b/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean index 536b8c470..25ab1a1b6 100644 --- a/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean +++ b/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean @@ -66,7 +66,7 @@ def ofSymmetric (f : E →ₗ[ℂ] E) (hf : f.IsSymmetric) : UnboundedOperator H @[simp] lemma ofSymmetric_apply {f : E →ₗ[ℂ] E} {hf : f.IsSymmetric} (ψ : E) : - (ofSymmetric (hE := hE) f hf).toLinearPMap ψ = E.subtypeL (f ψ) := rfl + (ofSymmetric (hE := hE) f hf).toLinearPMap ψ = E.subtypeL (f ψ) := rfl /-! ## Closure @@ -80,6 +80,7 @@ def closure : UnboundedOperator HS where lemma closure_toLinearPMap : U.closure.toLinearPMap = U.toLinearPMap.closure := rfl +/-- An unbounded operator is closed iff the graph of its defining LinearPMap is closed. -/ def IsClosed : Prop := U.toLinearPMap.IsClosed lemma closure_isClosed : U.closure.IsClosed := IsClosable.closure_isClosed U.is_closable @@ -114,6 +115,7 @@ lemma isSelfAdjoint_iff : IsSelfAdjoint U ↔ IsSelfAdjoint U.toLinearPMap := by lemma adjoint_isClosed : (U†).IsClosed := LinearPMap.adjoint_isClosed U.dense_domain +/-- The submodule of `WithLp 2 (HS × HS)` defined by `F`. -/ def submoduleToLp : Submodule ℂ (WithLp 2 (HS × HS)) where carrier := {x | x.ofLp ∈ F} add_mem' := by @@ -124,16 +126,15 @@ def submoduleToLp : Submodule ℂ (WithLp 2 (HS × HS)) where intro c x hx exact Submodule.smul_mem F c hx -lemma submoduleToLp_closure : - (submoduleToLp F.closure) = (submoduleToLp F).topologicalClosure := by +lemma submoduleToLp_closure : (submoduleToLp F.closure) = (submoduleToLp F).topologicalClosure := by rw [Submodule.ext_iff] simp [← Submodule.mem_closure_iff] -- Is this needed? intro x -- TODO: `toLp F.closure = (toLp F).closure` -- This is nontrivial: -- In `submoduleToLp F.closure` the closure is wrt the sup norm (by default `H × H` is equipped - -- with a norm defined as the supremum of the norms of their components). - -- In `(submoduleToLp F).closure` the closure is wrt the L² norm introduced above. + -- with a norm defined as the supremum of the norms of their components). + -- In `(submoduleToLp F).closure` the closure is wrt the L² norm introduced by `WithLp 2`. -- Need to use that `Lp` norms induce the same topology in two dimensions (two copies of `H`). sorry diff --git a/PhysLean/QuantumMechanics/DDimensions/SpaceDHilbertSpace/Basic.lean b/PhysLean/QuantumMechanics/DDimensions/SpaceDHilbertSpace/Basic.lean index e84b96f02..cd0e7e402 100644 --- a/PhysLean/QuantumMechanics/DDimensions/SpaceDHilbertSpace/Basic.lean +++ b/PhysLean/QuantumMechanics/DDimensions/SpaceDHilbertSpace/Basic.lean @@ -135,13 +135,13 @@ lemma mem_iff {f : Space d → ℂ} (hf : AEStronglyMeasurable f volume) : simp [h2, HasFiniteIntegral] lemma mk_add {f g : Space d → ℂ} {hf : MemHS f} {hg : MemHS g} : - mk (memHS_add hf hg) = mk hf + mk hg := rfl + mk (memHS_add hf hg) = mk hf + mk hg := rfl lemma mk_const_smul {f : Space d → ℂ} {c : ℂ} {hf : MemHS f} : - mk (memHS_const_smul (c := c) hf) = c • mk hf := rfl + mk (memHS_const_smul (c := c) hf) = c • mk hf := rfl lemma mk_eq_iff {f g : Space d → ℂ} {hf : MemHS f} {hg : MemHS g} : - mk hf = mk hg ↔ f =ᵐ[volume] g := by simp [mk] + mk hf = mk hg ↔ f =ᵐ[volume] g := by simp [mk] lemma ext_iff {f g : SpaceDHilbertSpace d} : f = g ↔ (f : Space d → ℂ) =ᵐ[volume] (g : Space d → ℂ) := Lp.ext_iff diff --git a/PhysLean/QuantumMechanics/DDimensions/SpaceDHilbertSpace/SchwartzSubmodule.lean b/PhysLean/QuantumMechanics/DDimensions/SpaceDHilbertSpace/SchwartzSubmodule.lean index 5876dd376..a87c27754 100644 --- a/PhysLean/QuantumMechanics/DDimensions/SpaceDHilbertSpace/SchwartzSubmodule.lean +++ b/PhysLean/QuantumMechanics/DDimensions/SpaceDHilbertSpace/SchwartzSubmodule.lean @@ -23,8 +23,8 @@ open SchwartzMap /-- The continuous linear map including Schwartz functions into `SpaceDHilbertSpace d`. -/ def schwartzIncl {d : ℕ} : 𝓢(Space d, ℂ) →L[ℂ] SpaceDHilbertSpace d := toLpCLM ℂ (E := Space d) ℂ 2 -lemma schwartzIncl_injective {d : ℕ} : - Function.Injective (schwartzIncl (d := d)) := injective_toLp (E := Space d) 2 +lemma schwartzIncl_injective {d : ℕ} : Function.Injective (schwartzIncl (d := d)) := + injective_toLp (E := Space d) 2 lemma schwartzIncl_coe_ae {d : ℕ} (f : 𝓢(Space d, ℂ)) : f.1 =ᵐ[volume] (schwartzIncl f) := (coeFn_toLp f 2).symm From 3e5cbf4faa134e047fbd9eb1c7b051d04a27d46c Mon Sep 17 00:00:00 2001 From: gloges Date: Mon, 23 Feb 2026 03:58:39 +0900 Subject: [PATCH 08/21] sorry removed: closable => adjoint dense --- .../DDimensions/Operators/Unbounded.lean | 91 +++++++++++++------ 1 file changed, 61 insertions(+), 30 deletions(-) diff --git a/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean b/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean index 25ab1a1b6..42266eed0 100644 --- a/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean +++ b/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean @@ -9,6 +9,10 @@ import PhysLean.QuantumMechanics.DDimensions.SpaceDHilbertSpace.SchwartzSubmodul # Unbounded operators +## References + +- K. Schmüdgen, "Unbounded Self-adjoint Operators on Hilbert Space", Part I. + -/ namespace QuantumMechanics @@ -51,7 +55,7 @@ instance : CoeFun (UnboundedOperator HS) lemma toFun_eq_coe (x : U.domain) : U.toFun x = U.toLinearPMap.toFun x := rfl /-! -## Construction of unbounded operators +### Construction of unbounded operators -/ /-- An `UnboundedOperator` constructed from a symmetric linear map on a dense submodule `E`. -/ @@ -69,7 +73,7 @@ lemma ofSymmetric_apply {f : E →ₗ[ℂ] E} {hf : f.IsSymmetric} (ψ : E) : (ofSymmetric (hE := hE) f hf).toLinearPMap ψ = E.subtypeL (f ψ) := rfl /-! -## Closure +### Closure -/ /-- The closure of an unbounded operator. -/ @@ -86,35 +90,9 @@ def IsClosed : Prop := U.toLinearPMap.IsClosed lemma closure_isClosed : U.closure.IsClosed := IsClosable.closure_isClosed U.is_closable /-! -## Adjoints +### Submodules of `HS × HS` -/ -/-- The adjoint of an unbounded operator, denoted as `U†`. -/ -def adjoint : UnboundedOperator HS where - toLinearPMap := U.toLinearPMap.adjoint - dense_domain := by - -- TODO: `U` is closable ⇒ `U†` is densely defined - sorry - is_closable := IsClosed.isClosable (adjoint_isClosed U.dense_domain) - -@[inherit_doc] -scoped postfix:1024 "†" => UnboundedOperator.adjoint - -instance instStar : Star (UnboundedOperator HS) where - star := fun U ↦ U.adjoint - -lemma adjoint_toLinearPMap : U†.toLinearPMap = U.toLinearPMap† := rfl - -lemma isSelfAdjoint_def : IsSelfAdjoint U ↔ U† = U := Iff.rfl - -lemma isSelfAdjoint_iff : IsSelfAdjoint U ↔ IsSelfAdjoint U.toLinearPMap := by - rw [isSelfAdjoint_def, LinearPMap.isSelfAdjoint_def] - constructor <;> intro h - · rw [← adjoint_toLinearPMap, h] - · rwa [UnboundedOperator.ext_iff, adjoint_toLinearPMap] - -lemma adjoint_isClosed : (U†).IsClosed := LinearPMap.adjoint_isClosed U.dense_domain - /-- The submodule of `WithLp 2 (HS × HS)` defined by `F`. -/ def submoduleToLp : Submodule ℂ (WithLp 2 (HS × HS)) where carrier := {x | x.ofLp ∈ F} @@ -200,6 +178,59 @@ lemma mem_submodule_closure_adjoint_iff_mem_submoduleToLp_closure_orthogonal : rw [submoduleToLp_closure] simp [← ClosedSubmodule.mem_toSubmodule_iff] +/-! +### Adjoints +-/ + +/-- The adjoint of an unbounded operator, denoted as `U†`. -/ +def adjoint : UnboundedOperator HS where + toLinearPMap := U.toLinearPMap.adjoint + dense_domain := by + by_contra hd + have hx : ∃ x ∈ U.toLinearPMap†.domainᗮ, x ≠ 0 := by + apply not_forall.mp at hd + rcases hd with ⟨y, hy⟩ + have hnetop : U.toLinearPMap†.domainᗮᗮ ≠ ⊤ := by + rw [Submodule.orthogonal_orthogonal_eq_closure] + exact Ne.symm (ne_of_mem_of_not_mem' trivial hy) + have hnebot : U.toLinearPMap†.domainᗮ ≠ ⊥ := by + by_contra + apply hnetop + rwa [Submodule.orthogonal_eq_top_iff] + exact Submodule.exists_mem_ne_zero_of_ne_bot hnebot + rcases hx with ⟨x, hx, hx'⟩ + apply hx' + apply graph_fst_eq_zero_snd U.toLinearPMap.closure _ rfl + rw [← IsClosable.graph_closure_eq_closure_graph U.is_closable] + rw [mem_submodule_closure_iff_mem_submoduleToLp_closure] + rw [← Submodule.orthogonal_orthogonal_eq_closure] + rw [← mem_submodule_adjoint_adjoint_iff_mem_submoduleToLp_orthogonal_orthogonal] + rw [← LinearPMap.adjoint_graph_eq_graph_adjoint U.dense_domain] + rw [mem_submodule_adjoint_iff_mem_submoduleToLp_orthogonal] + rintro ⟨y, Uy⟩ hy + simp only [neg_zero, WithLp.prod_inner_apply, inner_zero_right, add_zero] + apply hx y + exact mem_domain_of_mem_graph hy + is_closable := IsClosed.isClosable (adjoint_isClosed U.dense_domain) + +@[inherit_doc] +scoped postfix:1024 "†" => UnboundedOperator.adjoint + +instance instStar : Star (UnboundedOperator HS) where + star := fun U ↦ U.adjoint + +lemma adjoint_toLinearPMap : U†.toLinearPMap = U.toLinearPMap† := rfl + +lemma isSelfAdjoint_def : IsSelfAdjoint U ↔ U† = U := Iff.rfl + +lemma isSelfAdjoint_iff : IsSelfAdjoint U ↔ IsSelfAdjoint U.toLinearPMap := by + rw [isSelfAdjoint_def, LinearPMap.isSelfAdjoint_def] + constructor <;> intro h + · rw [← adjoint_toLinearPMap, h] + · rwa [UnboundedOperator.ext_iff, adjoint_toLinearPMap] + +lemma adjoint_isClosed : (U†).IsClosed := LinearPMap.adjoint_isClosed U.dense_domain + lemma closure_adjoint_eq_adjoint : U.closure† = U† := by -- Reduce to statement about graphs using density and closability assumptions apply UnboundedOperator.ext @@ -229,7 +260,7 @@ lemma adjoint_adjoint_eq_closure : U†† = U.closure := by rw [mem_submodule_closure_iff_mem_submoduleToLp_closure] /-! -## Generalized eigenvectors +### Generalized eigenvectors -/ /-- A map `F : D(U) →L[ℂ] ℂ` is a generalized eigenvector of an unbounded operator `U` From 8763deed7cc7e6641996287ae844f726394a39f4 Mon Sep 17 00:00:00 2001 From: gloges Date: Mon, 23 Feb 2026 04:27:05 +0900 Subject: [PATCH 09/21] sorry removed: symm + dense => closable --- .../QuantumMechanics/DDimensions/Operators/Unbounded.lean | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean b/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean index 42266eed0..4793b105b 100644 --- a/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean +++ b/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean @@ -63,10 +63,9 @@ def ofSymmetric (f : E →ₗ[ℂ] E) (hf : f.IsSymmetric) : UnboundedOperator H toLinearPMap := LinearPMap.mk E (E.subtype ∘ₗ f) dense_domain := hE is_closable := by - -- TODO: symmetric ∧ dense ⇒ closable - unfold Dense at hE - unfold LinearMap.IsSymmetric at hf - sorry + refine isClosable_iff_exists_closed_extension.mpr ?_ + use (LinearPMap.mk E (E.subtype ∘ₗ f))† + exact ⟨adjoint_isClosed hE, IsFormalAdjoint.le_adjoint hE hf⟩ @[simp] lemma ofSymmetric_apply {f : E →ₗ[ℂ] E} {hf : f.IsSymmetric} (ψ : E) : From b537d058d5c97775832c56ec0abc7a64be782a52 Mon Sep 17 00:00:00 2001 From: gloges Date: Mon, 23 Feb 2026 06:10:24 +0900 Subject: [PATCH 10/21] sorry-free --- .../DDimensions/Operators/Unbounded.lean | 72 ++++++++++++------- 1 file changed, 46 insertions(+), 26 deletions(-) diff --git a/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean b/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean index 4793b105b..a4608cd91 100644 --- a/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean +++ b/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean @@ -19,7 +19,7 @@ namespace QuantumMechanics noncomputable section -open LinearPMap +open LinearPMap Submodule /-- An `UnboundedOperator` is a linear map from a submodule of the Hilbert space to the Hilbert space, assumed to be both densely defined and closable. -/ @@ -103,22 +103,41 @@ def submoduleToLp : Submodule ℂ (WithLp 2 (HS × HS)) where intro c x hx exact Submodule.smul_mem F c hx +omit [CompleteSpace HS] in +lemma mem_submodule_iff_mem_submoduleToLp : + ∀ f, f ∈ F ↔ (WithLp.toLp 2 f) ∈ submoduleToLp F := fun _ => Eq.to_iff rfl + +omit [CompleteSpace HS] in lemma submoduleToLp_closure : (submoduleToLp F.closure) = (submoduleToLp F).topologicalClosure := by rw [Submodule.ext_iff] - simp [← Submodule.mem_closure_iff] -- Is this needed? intro x - -- TODO: `toLp F.closure = (toLp F).closure` - -- This is nontrivial: - -- In `submoduleToLp F.closure` the closure is wrt the sup norm (by default `H × H` is equipped - -- with a norm defined as the supremum of the norms of their components). - -- In `(submoduleToLp F).closure` the closure is wrt the L² norm introduced by `WithLp 2`. - -- Need to use that `Lp` norms induce the same topology in two dimensions (two copies of `H`). - sorry + rw [← mem_submodule_iff_mem_submoduleToLp] + change x.ofLp ∈ _root_.closure F ↔ x ∈ _root_.closure (submoduleToLp F) + repeat rw [mem_closure_iff_nhds] + constructor + · intro h t ht + apply mem_nhds_iff.mp at ht + rcases ht with ⟨t1, ht1, ht1', hx⟩ + have : ∃ t' ∈ nhds x.ofLp, (∀ y ∈ t', WithLp.toLp 2 y ∈ t1) := by + refine Filter.eventually_iff_exists_mem.mp ?_ + apply ContinuousAt.eventually_mem (by fun_prop) (IsOpen.mem_nhds ht1' hx) + rcases this with ⟨t2, ht2, ht2'⟩ + rcases h t2 ht2 with ⟨w, hw⟩ + use WithLp.toLp 2 w + exact ⟨Set.mem_preimage.mp (ht1 (ht2' w hw.1)), + (mem_submodule_iff_mem_submoduleToLp F w).mpr hw.2⟩ + · intro h t ht + apply mem_nhds_iff.mp at ht + rcases ht with ⟨t1, ht1, ht1', hx⟩ + have : ∃ t' ∈ nhds x, (∀ y ∈ t', y.ofLp ∈ t1) := by + refine Filter.eventually_iff_exists_mem.mp ?_ + exact ContinuousAt.eventually_mem (by fun_prop) (IsOpen.mem_nhds ht1' hx) + rcases this with ⟨t2, ht2, ht2'⟩ + rcases h t2 ht2 with ⟨w, hw⟩ + use w.ofLp + exact ⟨Set.mem_preimage.mp (ht1 (ht2' w hw.1)), (mem_toAddSubgroup (submoduleToLp F)).mp hw.2⟩ omit [CompleteSpace HS] in -lemma mem_submodule_iff_mem_submoduleToLp : - ∀ f, f ∈ F ↔ (WithLp.toLp 2 f) ∈ submoduleToLp F := fun _ => Eq.to_iff rfl - lemma mem_submodule_closure_iff_mem_submoduleToLp_closure : ∀ f, f ∈ F.topologicalClosure ↔ (WithLp.toLp 2 f) ∈ (submoduleToLp F).topologicalClosure := by intro f @@ -130,16 +149,16 @@ lemma mem_submodule_adjoint_iff_mem_submoduleToLp_orthogonal : ∀ f, f ∈ F.adjoint ↔ WithLp.toLp 2 (f.2, -f.1) ∈ (submoduleToLp F)ᗮ := by intro f constructor <;> intro h - · rw [Submodule.mem_orthogonal] + · rw [mem_orthogonal] intro u hu - rw [Submodule.mem_adjoint_iff] at h + rw [mem_adjoint_iff] at h have h' : inner ℂ u.snd f.1 = inner ℂ u.fst f.2 := by rw [← sub_eq_zero] exact h u.fst u.snd hu simp [h'] - · rw [Submodule.mem_adjoint_iff] + · rw [mem_adjoint_iff] intro a b hab - rw [Submodule.mem_orthogonal] at h + rw [mem_orthogonal] at h have hab' := (mem_submodule_iff_mem_submoduleToLp F (a, b)).mp hab have h' : inner ℂ a f.2 = inner ℂ b f.1 := by rw [← sub_eq_zero, sub_eq_add_neg, ← inner_neg_right] @@ -150,7 +169,7 @@ omit [CompleteSpace HS] in lemma mem_submodule_adjoint_adjoint_iff_mem_submoduleToLp_orthogonal_orthogonal : ∀ f, f ∈ F.adjoint.adjoint ↔ WithLp.toLp 2 f ∈ (submoduleToLp F)ᗮᗮ := by intro f - simp only [Submodule.mem_adjoint_iff] + simp only [mem_adjoint_iff] trans ∀ v, (∀ w ∈ submoduleToLp F, inner ℂ w v = 0) → inner ℂ v (WithLp.toLp 2 f) = 0 · constructor <;> intro h · intro v hw @@ -167,8 +186,9 @@ lemma mem_submodule_adjoint_adjoint_iff_mem_submoduleToLp_orthogonal_orthogonal have hw' := h' w.fst w.snd hw rw [sub_eq_zero] at hw' simp [hw'] - simp only [← Submodule.mem_orthogonal] + simp only [← mem_orthogonal] +omit [CompleteSpace HS] in lemma mem_submodule_closure_adjoint_iff_mem_submoduleToLp_closure_orthogonal : ∀ f, f ∈ F.closure.adjoint ↔ WithLp.toLp 2 (f.2, -f.1) ∈ (submoduleToLp F).closureᗮ := by intro f @@ -186,23 +206,23 @@ def adjoint : UnboundedOperator HS where toLinearPMap := U.toLinearPMap.adjoint dense_domain := by by_contra hd - have hx : ∃ x ∈ U.toLinearPMap†.domainᗮ, x ≠ 0 := by + have : ∃ x ∈ U.toLinearPMap†.domainᗮ, x ≠ 0 := by apply not_forall.mp at hd rcases hd with ⟨y, hy⟩ have hnetop : U.toLinearPMap†.domainᗮᗮ ≠ ⊤ := by - rw [Submodule.orthogonal_orthogonal_eq_closure] + rw [orthogonal_orthogonal_eq_closure] exact Ne.symm (ne_of_mem_of_not_mem' trivial hy) have hnebot : U.toLinearPMap†.domainᗮ ≠ ⊥ := by by_contra apply hnetop - rwa [Submodule.orthogonal_eq_top_iff] - exact Submodule.exists_mem_ne_zero_of_ne_bot hnebot - rcases hx with ⟨x, hx, hx'⟩ + rwa [orthogonal_eq_top_iff] + exact exists_mem_ne_zero_of_ne_bot hnebot + rcases this with ⟨x, hx, hx'⟩ apply hx' apply graph_fst_eq_zero_snd U.toLinearPMap.closure _ rfl rw [← IsClosable.graph_closure_eq_closure_graph U.is_closable] rw [mem_submodule_closure_iff_mem_submoduleToLp_closure] - rw [← Submodule.orthogonal_orthogonal_eq_closure] + rw [← orthogonal_orthogonal_eq_closure] rw [← mem_submodule_adjoint_adjoint_iff_mem_submoduleToLp_orthogonal_orthogonal] rw [← LinearPMap.adjoint_graph_eq_graph_adjoint U.dense_domain] rw [mem_submodule_adjoint_iff_mem_submoduleToLp_orthogonal] @@ -241,7 +261,7 @@ lemma closure_adjoint_eq_adjoint : U.closure† = U† := by ext f trans WithLp.toLp 2 (f.2, -f.1) ∈ (submoduleToLp U.toLinearPMap.graph).topologicalClosureᗮ · exact mem_submodule_closure_adjoint_iff_mem_submoduleToLp_closure_orthogonal _ _ - rw [Submodule.orthogonal_closure] + rw [orthogonal_closure] exact Iff.symm (mem_submodule_adjoint_iff_mem_submoduleToLp_orthogonal _ _) lemma adjoint_adjoint_eq_closure : U†† = U.closure := by @@ -255,7 +275,7 @@ lemma adjoint_adjoint_eq_closure : U†† = U.closure := by ext f trans WithLp.toLp 2 f ∈ (submoduleToLp U.toLinearPMap.graph)ᗮᗮ · exact mem_submodule_adjoint_adjoint_iff_mem_submoduleToLp_orthogonal_orthogonal _ _ - rw [Submodule.orthogonal_orthogonal_eq_closure] + rw [orthogonal_orthogonal_eq_closure] rw [mem_submodule_closure_iff_mem_submoduleToLp_closure] /-! From d03c6c149c31cc8f4195590b983bb2dd5d72e015 Mon Sep 17 00:00:00 2001 From: gloges Date: Mon, 23 Feb 2026 20:53:39 +0900 Subject: [PATCH 11/21] comments --- .../DDimensions/Operators/Unbounded.lean | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean b/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean index a4608cd91..0873c0aea 100644 --- a/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean +++ b/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean @@ -9,9 +9,21 @@ import PhysLean.QuantumMechanics.DDimensions.SpaceDHilbertSpace.SchwartzSubmodul # Unbounded operators +In this file we define +- `UnboundedOperator`: an unbounded operator with domain a submodule of a generic Hilbert space. + All unbounded operators are assumed to be both densely defined and closable. +- The closure, `UnboundedOperator.closure`, and adjoint, `UnboundedOperator.adjoint`, with notation + `U† = U.adjoint`. That `U†` is densely defined is guaranteed by the closability of `U`. +- The concept of a generalized eigenvector in `IsGeneralizedEigenvector`. + +We prove some basic relations, making use of the density and closability assumptions: +- `U.closure† = U†` in `closure_adjoint_eq_adjoint` +- `U†† = U.closure` in `adjoint_adjoint_eq_closure` + ## References -- K. Schmüdgen, "Unbounded Self-adjoint Operators on Hilbert Space", Part I. +- K. Schmüdgen, (2012). "Unbounded self-adjoint operators on Hilbert space" (Vol. 265). Springer. + https://doi.org/10.1007/978-94-007-4753-1 -/ From ef6f0e212fd38e2e97bad387744d672eb558d060 Mon Sep 17 00:00:00 2001 From: gloges Date: Wed, 25 Feb 2026 01:15:38 +0900 Subject: [PATCH 12/21] UnboundedOperator extends LinearPMap --- .../DDimensions/Operators/Unbounded.lean | 41 +++++++++++-------- 1 file changed, 23 insertions(+), 18 deletions(-) diff --git a/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean b/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean index 0873c0aea..588ff8908 100644 --- a/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean +++ b/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean @@ -37,12 +37,11 @@ open LinearPMap Submodule to the Hilbert space, assumed to be both densely defined and closable. -/ @[ext] structure UnboundedOperator - (HS : Type) [NormedAddCommGroup HS] [InnerProductSpace ℂ HS] [CompleteSpace HS] where - /-- The LinearPMap defining the unbounded operator. -/ - toLinearPMap : LinearPMap ℂ HS HS - /-- The domain of the unbounded operator is dense in the Hilbert space. -/ - dense_domain : Dense (toLinearPMap.domain : Set HS) - /-- The unbounded operator is closable. -/ + (HS : Type) [NormedAddCommGroup HS] [InnerProductSpace ℂ HS] [CompleteSpace HS] + extends LinearPMap ℂ HS HS where + /-- The domain of an unbounded operator is dense in the Hilbert space. -/ + dense_domain : Dense (domain : Set HS) + /-- An unbounded operator is closable. -/ is_closable : toLinearPMap.IsClosable namespace UnboundedOperator @@ -53,19 +52,27 @@ variable {E : Submodule ℂ HS} {hE : Dense (E : Set HS)} (F : Submodule ℂ (HS × HS)) -/-- Domain of `UnboundedOperator`. -/ -def domain : Submodule ℂ HS := U.toLinearPMap.domain - /-- `UnboundedOperator` as a function. -/ @[coe] -def toFun : U.domain → HS := U.toLinearPMap.toFun +def toFun' : U.domain → HS := U.toLinearPMap.toFun instance : CoeFun (UnboundedOperator HS) - (fun U : UnboundedOperator HS ↦ U.domain → HS) := ⟨toFun⟩ + (fun U : UnboundedOperator HS ↦ U.domain → HS) := ⟨toFun'⟩ @[simp] lemma toFun_eq_coe (x : U.domain) : U.toFun x = U.toLinearPMap.toFun x := rfl +lemma ext' (U T : UnboundedOperator HS) : U.toLinearPMap = T.toLinearPMap → U = T := by + intro h + apply UnboundedOperator.ext + · exact toSubMulAction_inj.mp (congrArg toSubMulAction (congrArg domain h)) + · exact congr_arg_heq toFun h + +lemma ext_iff' (U T : UnboundedOperator HS) : U = T ↔ U.toLinearPMap = T.toLinearPMap := by + refine ⟨?_, UnboundedOperator.ext' U T⟩ + intro h + rw [h] + /-! ### Construction of unbounded operators -/ @@ -81,7 +88,7 @@ def ofSymmetric (f : E →ₗ[ℂ] E) (hf : f.IsSymmetric) : UnboundedOperator H @[simp] lemma ofSymmetric_apply {f : E →ₗ[ℂ] E} {hf : f.IsSymmetric} (ψ : E) : - (ofSymmetric (hE := hE) f hf).toLinearPMap ψ = E.subtypeL (f ψ) := rfl + (ofSymmetric (hE := hE) f hf) ψ = E.subtypeL (f ψ) := rfl /-! ### Closure @@ -255,16 +262,14 @@ lemma adjoint_toLinearPMap : U†.toLinearPMap = U.toLinearPMap† := rfl lemma isSelfAdjoint_def : IsSelfAdjoint U ↔ U† = U := Iff.rfl lemma isSelfAdjoint_iff : IsSelfAdjoint U ↔ IsSelfAdjoint U.toLinearPMap := by - rw [isSelfAdjoint_def, LinearPMap.isSelfAdjoint_def] - constructor <;> intro h - · rw [← adjoint_toLinearPMap, h] - · rwa [UnboundedOperator.ext_iff, adjoint_toLinearPMap] + rw [isSelfAdjoint_def, LinearPMap.isSelfAdjoint_def, ← adjoint_toLinearPMap] + exact UnboundedOperator.ext_iff' U† U lemma adjoint_isClosed : (U†).IsClosed := LinearPMap.adjoint_isClosed U.dense_domain lemma closure_adjoint_eq_adjoint : U.closure† = U† := by -- Reduce to statement about graphs using density and closability assumptions - apply UnboundedOperator.ext + apply UnboundedOperator.ext' apply LinearPMap.eq_of_eq_graph rw [adjoint_toLinearPMap, adjoint_graph_eq_graph_adjoint U.closure.dense_domain] rw [adjoint_toLinearPMap, adjoint_graph_eq_graph_adjoint U.dense_domain] @@ -278,7 +283,7 @@ lemma closure_adjoint_eq_adjoint : U.closure† = U† := by lemma adjoint_adjoint_eq_closure : U†† = U.closure := by -- Reduce to statement about graphs using density and closability assumptions - apply UnboundedOperator.ext + apply UnboundedOperator.ext' apply LinearPMap.eq_of_eq_graph rw [adjoint_toLinearPMap, adjoint_graph_eq_graph_adjoint U†.dense_domain] rw [adjoint_toLinearPMap, adjoint_graph_eq_graph_adjoint U.dense_domain] From 93d97b2583c52f4a08de951f54e01b0374ed4e46 Mon Sep 17 00:00:00 2001 From: gloges Date: Wed, 25 Feb 2026 09:55:27 +0900 Subject: [PATCH 13/21] remove unnecessary coe --- PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean | 3 --- 1 file changed, 3 deletions(-) diff --git a/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean b/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean index 588ff8908..676c649fe 100644 --- a/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean +++ b/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean @@ -59,9 +59,6 @@ def toFun' : U.domain → HS := U.toLinearPMap.toFun instance : CoeFun (UnboundedOperator HS) (fun U : UnboundedOperator HS ↦ U.domain → HS) := ⟨toFun'⟩ -@[simp] -lemma toFun_eq_coe (x : U.domain) : U.toFun x = U.toLinearPMap.toFun x := rfl - lemma ext' (U T : UnboundedOperator HS) : U.toLinearPMap = T.toLinearPMap → U = T := by intro h apply UnboundedOperator.ext From 749c02b6f4cae465f93d69b1e3999e695c3e3386 Mon Sep 17 00:00:00 2001 From: gloges Date: Wed, 25 Feb 2026 21:25:30 +0900 Subject: [PATCH 14/21] relocate submodule lemmas --- PhysLean.lean | 1 + .../InnerProductSpace/Submodule.lean | 121 ++++++++++++++++++ .../DDimensions/Operators/Unbounded.lean | 111 +--------------- 3 files changed, 123 insertions(+), 110 deletions(-) create mode 100644 PhysLean/Mathematics/InnerProductSpace/Submodule.lean diff --git a/PhysLean.lean b/PhysLean.lean index 00f4422fc..b45cee7ae 100644 --- a/PhysLean.lean +++ b/PhysLean.lean @@ -57,6 +57,7 @@ import PhysLean.Mathematics.Geometry.Metric.Riemannian.Defs import PhysLean.Mathematics.InnerProductSpace.Adjoint import PhysLean.Mathematics.InnerProductSpace.Basic import PhysLean.Mathematics.InnerProductSpace.Calculus +import PhysLean.Mathematics.InnerProductSpace.Submodule import PhysLean.Mathematics.KroneckerDelta import PhysLean.Mathematics.LinearMaps import PhysLean.Mathematics.List diff --git a/PhysLean/Mathematics/InnerProductSpace/Submodule.lean b/PhysLean/Mathematics/InnerProductSpace/Submodule.lean new file mode 100644 index 000000000..2360fafae --- /dev/null +++ b/PhysLean/Mathematics/InnerProductSpace/Submodule.lean @@ -0,0 +1,121 @@ +/- +Copyright (c) 2026 Gregory J. Loges. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Gregory J. Loges +-/ +import Mathlib.Analysis.InnerProductSpace.LinearPMap +/-! + +# Submodules of `E × E` + +In this module we define `submoduleToLp` which reinterprets a submodule of `E × E`, +where `E` is an inner product space, as a submodule of `WithLp 2 (E × E)`. +This allows us to take advantage of the inner product structure, since otherwise +by default `E × E` is given the sup norm. + +-/ + +namespace InnerProductSpaceSubmodule + +open LinearPMap Submodule + +variable + {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℂ E] + (M : Submodule ℂ (E × E)) + +/-- The submodule of `WithLp 2 (E × E)` defined by `M`. -/ +def submoduleToLp : Submodule ℂ (WithLp 2 (E × E)) where + carrier := {x | x.ofLp ∈ M} + add_mem' := by + intro a b ha hb + exact Submodule.add_mem M ha hb + zero_mem' := Submodule.zero_mem M + smul_mem' := by + intro c x hx + exact Submodule.smul_mem M c hx + +lemma mem_submodule_iff_mem_submoduleToLp (f : E × E): + f ∈ M ↔ (WithLp.toLp 2 f) ∈ submoduleToLp M := Eq.to_iff rfl + +lemma submoduleToLp_closure : (submoduleToLp M.closure) = (submoduleToLp M).topologicalClosure := by + rw [Submodule.ext_iff] + intro x + rw [← mem_submodule_iff_mem_submoduleToLp] + change x.ofLp ∈ _root_.closure M ↔ x ∈ _root_.closure (submoduleToLp M) + repeat rw [mem_closure_iff_nhds] + constructor + · intro h t ht + apply mem_nhds_iff.mp at ht + rcases ht with ⟨t1, ht1, ht1', hx⟩ + have : ∃ t' ∈ nhds x.ofLp, (∀ y ∈ t', WithLp.toLp 2 y ∈ t1) := by + refine Filter.eventually_iff_exists_mem.mp ?_ + apply ContinuousAt.eventually_mem (by fun_prop) (IsOpen.mem_nhds ht1' hx) + rcases this with ⟨t2, ht2, ht2'⟩ + rcases h t2 ht2 with ⟨w, hw⟩ + use WithLp.toLp 2 w + exact ⟨Set.mem_preimage.mp (ht1 (ht2' w hw.1)), + (mem_submodule_iff_mem_submoduleToLp M w).mpr hw.2⟩ + · intro h t ht + apply mem_nhds_iff.mp at ht + rcases ht with ⟨t1, ht1, ht1', hx⟩ + have : ∃ t' ∈ nhds x, (∀ y ∈ t', y.ofLp ∈ t1) := by + refine Filter.eventually_iff_exists_mem.mp ?_ + exact ContinuousAt.eventually_mem (by fun_prop) (IsOpen.mem_nhds ht1' hx) + rcases this with ⟨t2, ht2, ht2'⟩ + rcases h t2 ht2 with ⟨w, hw⟩ + use w.ofLp + exact ⟨Set.mem_preimage.mp (ht1 (ht2' w hw.1)), (mem_toAddSubgroup (submoduleToLp M)).mp hw.2⟩ + +lemma mem_submodule_closure_iff_mem_submoduleToLp_closure (f : E × E): + f ∈ M.topologicalClosure ↔ (WithLp.toLp 2 f) ∈ (submoduleToLp M).topologicalClosure := by + rw [← submoduleToLp_closure] + rfl + +lemma mem_submodule_adjoint_iff_mem_submoduleToLp_orthogonal (f : E × E) : + f ∈ M.adjoint ↔ WithLp.toLp 2 (f.2, -f.1) ∈ (submoduleToLp M)ᗮ := by + constructor <;> intro h + · rw [mem_orthogonal] + intro u hu + rw [mem_adjoint_iff] at h + have h' : inner ℂ u.snd f.1 = inner ℂ u.fst f.2 := by + rw [← sub_eq_zero] + exact h u.fst u.snd hu + simp [h'] + · rw [mem_adjoint_iff] + intro a b hab + rw [mem_orthogonal] at h + have hab' := (mem_submodule_iff_mem_submoduleToLp M (a, b)).mp hab + have h' : inner ℂ a f.2 = inner ℂ b f.1 := by + rw [← sub_eq_zero, sub_eq_add_neg, ← inner_neg_right] + exact h (WithLp.toLp 2 (a, b)) hab' + simp [h'] + +lemma mem_submodule_adjoint_adjoint_iff_mem_submoduleToLp_orthogonal_orthogonal (f : E × E) : + f ∈ M.adjoint.adjoint ↔ WithLp.toLp 2 f ∈ (submoduleToLp M)ᗮᗮ := by + simp only [mem_adjoint_iff] + trans ∀ v, (∀ w ∈ submoduleToLp M, inner ℂ w v = 0) → inner ℂ v (WithLp.toLp 2 f) = 0 + · constructor <;> intro h + · intro v hw + have h' := h (-v.snd) v.fst + rw [inner_neg_left, sub_neg_eq_add] at h' + apply h' + intro a b hab + rw [inner_neg_right, neg_sub_left, neg_eq_zero] + exact hw (WithLp.toLp 2 (a, b)) ((mem_submodule_iff_mem_submoduleToLp M (a, b)).mp hab) + · intro a b h' + rw [sub_eq_add_neg, ← inner_neg_left] + apply h (WithLp.toLp 2 (b, -a)) + intro w hw + have hw' := h' w.fst w.snd hw + rw [sub_eq_zero] at hw' + simp [hw'] + simp only [← mem_orthogonal] + +lemma mem_submodule_closure_adjoint_iff_mem_submoduleToLp_closure_orthogonal (f : E × E): + f ∈ M.closure.adjoint ↔ WithLp.toLp 2 (f.2, -f.1) ∈ (submoduleToLp M).closureᗮ := by + trans (WithLp.toLp 2 (f.2, -f.1)) ∈ (submoduleToLp M.closure)ᗮ + · apply mem_submodule_adjoint_iff_mem_submoduleToLp_orthogonal M.closure f + rw [submoduleToLp_closure] + simp [← ClosedSubmodule.mem_toSubmodule_iff] + +end InnerProductSpaceSubmodule diff --git a/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean b/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean index 676c649fe..b82e0145b 100644 --- a/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean +++ b/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean @@ -3,7 +3,7 @@ Copyright (c) 2026 Gregory J. Loges. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Gregory J. Loges -/ -import Mathlib.Analysis.InnerProductSpace.LinearPMap +import PhysLean.Mathematics.InnerProductSpace.Submodule import PhysLean.QuantumMechanics.DDimensions.SpaceDHilbertSpace.SchwartzSubmodule /-! @@ -104,115 +104,6 @@ def IsClosed : Prop := U.toLinearPMap.IsClosed lemma closure_isClosed : U.closure.IsClosed := IsClosable.closure_isClosed U.is_closable -/-! -### Submodules of `HS × HS` --/ - -/-- The submodule of `WithLp 2 (HS × HS)` defined by `F`. -/ -def submoduleToLp : Submodule ℂ (WithLp 2 (HS × HS)) where - carrier := {x | x.ofLp ∈ F} - add_mem' := by - intro a b ha hb - exact Submodule.add_mem F ha hb - zero_mem' := Submodule.zero_mem F - smul_mem' := by - intro c x hx - exact Submodule.smul_mem F c hx - -omit [CompleteSpace HS] in -lemma mem_submodule_iff_mem_submoduleToLp : - ∀ f, f ∈ F ↔ (WithLp.toLp 2 f) ∈ submoduleToLp F := fun _ => Eq.to_iff rfl - -omit [CompleteSpace HS] in -lemma submoduleToLp_closure : (submoduleToLp F.closure) = (submoduleToLp F).topologicalClosure := by - rw [Submodule.ext_iff] - intro x - rw [← mem_submodule_iff_mem_submoduleToLp] - change x.ofLp ∈ _root_.closure F ↔ x ∈ _root_.closure (submoduleToLp F) - repeat rw [mem_closure_iff_nhds] - constructor - · intro h t ht - apply mem_nhds_iff.mp at ht - rcases ht with ⟨t1, ht1, ht1', hx⟩ - have : ∃ t' ∈ nhds x.ofLp, (∀ y ∈ t', WithLp.toLp 2 y ∈ t1) := by - refine Filter.eventually_iff_exists_mem.mp ?_ - apply ContinuousAt.eventually_mem (by fun_prop) (IsOpen.mem_nhds ht1' hx) - rcases this with ⟨t2, ht2, ht2'⟩ - rcases h t2 ht2 with ⟨w, hw⟩ - use WithLp.toLp 2 w - exact ⟨Set.mem_preimage.mp (ht1 (ht2' w hw.1)), - (mem_submodule_iff_mem_submoduleToLp F w).mpr hw.2⟩ - · intro h t ht - apply mem_nhds_iff.mp at ht - rcases ht with ⟨t1, ht1, ht1', hx⟩ - have : ∃ t' ∈ nhds x, (∀ y ∈ t', y.ofLp ∈ t1) := by - refine Filter.eventually_iff_exists_mem.mp ?_ - exact ContinuousAt.eventually_mem (by fun_prop) (IsOpen.mem_nhds ht1' hx) - rcases this with ⟨t2, ht2, ht2'⟩ - rcases h t2 ht2 with ⟨w, hw⟩ - use w.ofLp - exact ⟨Set.mem_preimage.mp (ht1 (ht2' w hw.1)), (mem_toAddSubgroup (submoduleToLp F)).mp hw.2⟩ - -omit [CompleteSpace HS] in -lemma mem_submodule_closure_iff_mem_submoduleToLp_closure : - ∀ f, f ∈ F.topologicalClosure ↔ (WithLp.toLp 2 f) ∈ (submoduleToLp F).topologicalClosure := by - intro f - rw [← submoduleToLp_closure] - rfl - -omit [CompleteSpace HS] in -lemma mem_submodule_adjoint_iff_mem_submoduleToLp_orthogonal : - ∀ f, f ∈ F.adjoint ↔ WithLp.toLp 2 (f.2, -f.1) ∈ (submoduleToLp F)ᗮ := by - intro f - constructor <;> intro h - · rw [mem_orthogonal] - intro u hu - rw [mem_adjoint_iff] at h - have h' : inner ℂ u.snd f.1 = inner ℂ u.fst f.2 := by - rw [← sub_eq_zero] - exact h u.fst u.snd hu - simp [h'] - · rw [mem_adjoint_iff] - intro a b hab - rw [mem_orthogonal] at h - have hab' := (mem_submodule_iff_mem_submoduleToLp F (a, b)).mp hab - have h' : inner ℂ a f.2 = inner ℂ b f.1 := by - rw [← sub_eq_zero, sub_eq_add_neg, ← inner_neg_right] - exact h (WithLp.toLp 2 (a, b)) hab' - simp [h'] - -omit [CompleteSpace HS] in -lemma mem_submodule_adjoint_adjoint_iff_mem_submoduleToLp_orthogonal_orthogonal : - ∀ f, f ∈ F.adjoint.adjoint ↔ WithLp.toLp 2 f ∈ (submoduleToLp F)ᗮᗮ := by - intro f - simp only [mem_adjoint_iff] - trans ∀ v, (∀ w ∈ submoduleToLp F, inner ℂ w v = 0) → inner ℂ v (WithLp.toLp 2 f) = 0 - · constructor <;> intro h - · intro v hw - have h' := h (-v.snd) v.fst - rw [inner_neg_left, sub_neg_eq_add] at h' - apply h' - intro a b hab - rw [inner_neg_right, neg_sub_left, neg_eq_zero] - exact hw (WithLp.toLp 2 (a, b)) ((mem_submodule_iff_mem_submoduleToLp F (a, b)).mp hab) - · intro a b h' - rw [sub_eq_add_neg, ← inner_neg_left] - apply h (WithLp.toLp 2 (b, -a)) - intro w hw - have hw' := h' w.fst w.snd hw - rw [sub_eq_zero] at hw' - simp [hw'] - simp only [← mem_orthogonal] - -omit [CompleteSpace HS] in -lemma mem_submodule_closure_adjoint_iff_mem_submoduleToLp_closure_orthogonal : - ∀ f, f ∈ F.closure.adjoint ↔ WithLp.toLp 2 (f.2, -f.1) ∈ (submoduleToLp F).closureᗮ := by - intro f - trans (WithLp.toLp 2 (f.2, -f.1)) ∈ (submoduleToLp F.closure)ᗮ - · apply mem_submodule_adjoint_iff_mem_submoduleToLp_orthogonal F.closure f - rw [submoduleToLp_closure] - simp [← ClosedSubmodule.mem_toSubmodule_iff] - /-! ### Adjoints -/ From e9702d077bfd295d8774585d217e5be6430b6074 Mon Sep 17 00:00:00 2001 From: gloges Date: Wed, 25 Feb 2026 21:29:41 +0900 Subject: [PATCH 15/21] style improvements --- .../DDimensions/SpaceDHilbertSpace/Basic.lean | 8 +++++--- .../DDimensions/SpaceDHilbertSpace/SchwartzSubmodule.lean | 7 ++----- 2 files changed, 7 insertions(+), 8 deletions(-) diff --git a/PhysLean/QuantumMechanics/DDimensions/SpaceDHilbertSpace/Basic.lean b/PhysLean/QuantumMechanics/DDimensions/SpaceDHilbertSpace/Basic.lean index cd0e7e402..0e0ec1ac0 100644 --- a/PhysLean/QuantumMechanics/DDimensions/SpaceDHilbertSpace/Basic.lean +++ b/PhysLean/QuantumMechanics/DDimensions/SpaceDHilbertSpace/Basic.lean @@ -104,7 +104,7 @@ lemma coe_hilbertSpace_memHS (f : SpaceDHilbertSpace d) : MemHS (f : Space d → exact hf ▸ f.2 lemma mk_surjective (f : SpaceDHilbertSpace d) : - ∃ (g : Space d → ℂ), ∃ (hg : MemHS g), mk hg = f := by + ∃ (g : Space d → ℂ) (hg : MemHS g), mk hg = f := by use f, coe_hilbertSpace_memHS f simp [mk] @@ -129,14 +129,16 @@ lemma mem_iff {f : Space d → ℂ} (hf : AEStronglyMeasurable f volume) : have h2 : AEStronglyMeasurable (fun x ↦ norm (f x) ^ 2) := AEStronglyMeasurable.pow (continuous_norm.comp_aestronglyMeasurable hf) 2 - simp only [h1, true_and, Integrable] + simp only [h1] simp only [eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top (NeZero.ne' 2).symm (ENNReal.top_ne_ofNat).symm, ENNReal.toReal_ofNat, ENNReal.rpow_ofNat] - simp [h2, HasFiniteIntegral] + simp [h2, Integrable, HasFiniteIntegral] +@[simp] lemma mk_add {f g : Space d → ℂ} {hf : MemHS f} {hg : MemHS g} : mk (memHS_add hf hg) = mk hf + mk hg := rfl +@[simp] lemma mk_const_smul {f : Space d → ℂ} {c : ℂ} {hf : MemHS f} : mk (memHS_const_smul (c := c) hf) = c • mk hf := rfl diff --git a/PhysLean/QuantumMechanics/DDimensions/SpaceDHilbertSpace/SchwartzSubmodule.lean b/PhysLean/QuantumMechanics/DDimensions/SpaceDHilbertSpace/SchwartzSubmodule.lean index a87c27754..b7e25c449 100644 --- a/PhysLean/QuantumMechanics/DDimensions/SpaceDHilbertSpace/SchwartzSubmodule.lean +++ b/PhysLean/QuantumMechanics/DDimensions/SpaceDHilbertSpace/SchwartzSubmodule.lean @@ -32,11 +32,8 @@ lemma schwartzIncl_coe_ae {d : ℕ} (f : 𝓢(Space d, ℂ)) : f.1 =ᵐ[volume] lemma schwartzIncl_inner {d : ℕ} (f g : 𝓢(Space d, ℂ)) : ⟪schwartzIncl f, schwartzIncl g⟫_ℂ = ∫ x : Space d, starRingEnd ℂ (f x) * g x := by apply integral_congr_ae - have hf := schwartzIncl_coe_ae f - have hg := schwartzIncl_coe_ae g - filter_upwards [hf, hg] with _ hf hg - rw [← hf, ← hg] - rw [RCLike.inner_apply, mul_comm] + filter_upwards [schwartzIncl_coe_ae f, schwartzIncl_coe_ae g] with _ hf hg + rw [← hf, ← hg, RCLike.inner_apply, mul_comm] rfl /-- The submodule of `SpaceDHilbertSpace d` consisting of Schwartz functions. -/ From add99dfee4741fe36d992ca398a4c84196aecb21 Mon Sep 17 00:00:00 2001 From: gloges Date: Wed, 25 Feb 2026 21:30:16 +0900 Subject: [PATCH 16/21] more improvements --- .../DDimensions/Operators/Unbounded.lean | 60 +++++++++---------- 1 file changed, 30 insertions(+), 30 deletions(-) diff --git a/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean b/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean index b82e0145b..ac9402d8c 100644 --- a/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean +++ b/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean @@ -29,15 +29,13 @@ We prove some basic relations, making use of the density and closability assumpt namespace QuantumMechanics -noncomputable section - open LinearPMap Submodule /-- An `UnboundedOperator` is a linear map from a submodule of the Hilbert space to the Hilbert space, assumed to be both densely defined and closable. -/ @[ext] structure UnboundedOperator - (HS : Type) [NormedAddCommGroup HS] [InnerProductSpace ℂ HS] [CompleteSpace HS] + (HS : Type*) [NormedAddCommGroup HS] [InnerProductSpace ℂ HS] [CompleteSpace HS] extends LinearPMap ℂ HS HS where /-- The domain of an unbounded operator is dense in the Hilbert space. -/ dense_domain : Dense (domain : Set HS) @@ -47,20 +45,10 @@ structure UnboundedOperator namespace UnboundedOperator variable - {HS : Type} [NormedAddCommGroup HS] [InnerProductSpace ℂ HS] [CompleteSpace HS] + {HS : Type*} [NormedAddCommGroup HS] [InnerProductSpace ℂ HS] [CompleteSpace HS] (U : UnboundedOperator HS) - {E : Submodule ℂ HS} {hE : Dense (E : Set HS)} - (F : Submodule ℂ (HS × HS)) - -/-- `UnboundedOperator` as a function. -/ -@[coe] -def toFun' : U.domain → HS := U.toLinearPMap.toFun - -instance : CoeFun (UnboundedOperator HS) - (fun U : UnboundedOperator HS ↦ U.domain → HS) := ⟨toFun'⟩ -lemma ext' (U T : UnboundedOperator HS) : U.toLinearPMap = T.toLinearPMap → U = T := by - intro h +lemma ext' (U T : UnboundedOperator HS) (h : U.toLinearPMap = T.toLinearPMap) : U = T := by apply UnboundedOperator.ext · exact toSubMulAction_inj.mp (congrArg toSubMulAction (congrArg domain h)) · exact congr_arg_heq toFun h @@ -74,6 +62,8 @@ lemma ext_iff' (U T : UnboundedOperator HS) : U = T ↔ U.toLinearPMap = T.toLin ### Construction of unbounded operators -/ +variable {E : Submodule ℂ HS} {hE : Dense (E : Set HS)} + /-- An `UnboundedOperator` constructed from a symmetric linear map on a dense submodule `E`. -/ def ofSymmetric (f : E →ₗ[ℂ] E) (hf : f.IsSymmetric) : UnboundedOperator HS where toLinearPMap := LinearPMap.mk E (E.subtype ∘ₗ f) @@ -85,18 +75,21 @@ def ofSymmetric (f : E →ₗ[ℂ] E) (hf : f.IsSymmetric) : UnboundedOperator H @[simp] lemma ofSymmetric_apply {f : E →ₗ[ℂ] E} {hf : f.IsSymmetric} (ψ : E) : - (ofSymmetric (hE := hE) f hf) ψ = E.subtypeL (f ψ) := rfl + (ofSymmetric (hE := hE) f hf).toLinearPMap ψ = E.subtypeL (f ψ) := rfl /-! ### Closure -/ +section Closure + /-- The closure of an unbounded operator. -/ -def closure : UnboundedOperator HS where +noncomputable def closure : UnboundedOperator HS where toLinearPMap := U.toLinearPMap.closure dense_domain := Dense.mono (HasCore.le_domain (closureHasCore U.toLinearPMap)) U.dense_domain is_closable := IsClosed.isClosable (IsClosable.closure_isClosed U.is_closable) +@[simp] lemma closure_toLinearPMap : U.closure.toLinearPMap = U.toLinearPMap.closure := rfl /-- An unbounded operator is closed iff the graph of its defining LinearPMap is closed. -/ @@ -104,12 +97,18 @@ def IsClosed : Prop := U.toLinearPMap.IsClosed lemma closure_isClosed : U.closure.IsClosed := IsClosable.closure_isClosed U.is_closable +end Closure + /-! ### Adjoints -/ +section Adjoints + +open InnerProductSpaceSubmodule + /-- The adjoint of an unbounded operator, denoted as `U†`. -/ -def adjoint : UnboundedOperator HS where +noncomputable def adjoint : UnboundedOperator HS where toLinearPMap := U.toLinearPMap.adjoint dense_domain := by by_contra hd @@ -127,12 +126,12 @@ def adjoint : UnboundedOperator HS where rcases this with ⟨x, hx, hx'⟩ apply hx' apply graph_fst_eq_zero_snd U.toLinearPMap.closure _ rfl - rw [← IsClosable.graph_closure_eq_closure_graph U.is_closable] - rw [mem_submodule_closure_iff_mem_submoduleToLp_closure] - rw [← orthogonal_orthogonal_eq_closure] - rw [← mem_submodule_adjoint_adjoint_iff_mem_submoduleToLp_orthogonal_orthogonal] - rw [← LinearPMap.adjoint_graph_eq_graph_adjoint U.dense_domain] - rw [mem_submodule_adjoint_iff_mem_submoduleToLp_orthogonal] + rw [← IsClosable.graph_closure_eq_closure_graph U.is_closable, + mem_submodule_closure_iff_mem_submoduleToLp_closure, + ← orthogonal_orthogonal_eq_closure, + ← mem_submodule_adjoint_adjoint_iff_mem_submoduleToLp_orthogonal_orthogonal, + ← LinearPMap.adjoint_graph_eq_graph_adjoint U.dense_domain, + mem_submodule_adjoint_iff_mem_submoduleToLp_orthogonal] rintro ⟨y, Uy⟩ hy simp only [neg_zero, WithLp.prod_inner_apply, inner_zero_right, add_zero] apply hx y @@ -142,9 +141,10 @@ def adjoint : UnboundedOperator HS where @[inherit_doc] scoped postfix:1024 "†" => UnboundedOperator.adjoint -instance instStar : Star (UnboundedOperator HS) where +noncomputable instance instStar : Star (UnboundedOperator HS) where star := fun U ↦ U.adjoint +@[simp] lemma adjoint_toLinearPMap : U†.toLinearPMap = U.toLinearPMap† := rfl lemma isSelfAdjoint_def : IsSelfAdjoint U ↔ U† = U := Iff.rfl @@ -180,8 +180,9 @@ lemma adjoint_adjoint_eq_closure : U†† = U.closure := by ext f trans WithLp.toLp 2 f ∈ (submoduleToLp U.toLinearPMap.graph)ᗮᗮ · exact mem_submodule_adjoint_adjoint_iff_mem_submoduleToLp_orthogonal_orthogonal _ _ - rw [orthogonal_orthogonal_eq_closure] - rw [mem_submodule_closure_iff_mem_submoduleToLp_closure] + rw [orthogonal_orthogonal_eq_closure, mem_submodule_closure_iff_mem_submoduleToLp_closure] + +end Adjoints /-! ### Generalized eigenvectors @@ -190,10 +191,10 @@ lemma adjoint_adjoint_eq_closure : U†† = U.closure := by /-- A map `F : D(U) →L[ℂ] ℂ` is a generalized eigenvector of an unbounded operator `U` if there is an eigenvalue `c` such that for all `ψ ∈ D(U)`, `F (U ψ) = c ⬝ F ψ`. -/ def IsGeneralizedEigenvector (F : U.domain →L[ℂ] ℂ) (c : ℂ) : Prop := - ∀ ψ : U.domain, ∃ ψ' : U.domain, ψ' = U ψ ∧ F ψ' = c • F ψ + ∀ ψ : U.domain, ∃ ψ' : U.domain, ψ' = U.toFun ψ ∧ F ψ' = c • F ψ lemma isGeneralizedEigenvector_ofSymmetric_iff - {f : E →ₗ[ℂ] E} {hf : f.IsSymmetric} (F : E →L[ℂ] ℂ) (c : ℂ) : + {f : E →ₗ[ℂ] E} (hf : f.IsSymmetric) (F : E →L[ℂ] ℂ) (c : ℂ) : IsGeneralizedEigenvector (ofSymmetric (hE := hE) f hf) F c ↔ ∀ ψ : E, F (f ψ) = c • F ψ := by constructor <;> intro h ψ · obtain ⟨ψ', hψ', hψ''⟩ := h ψ @@ -204,5 +205,4 @@ lemma isGeneralizedEigenvector_ofSymmetric_iff exact ⟨by simp, h ψ⟩ end UnboundedOperator -end end QuantumMechanics From c4e997c9eb3fcfcd848e5c0dc6beb7fa8ccb1e54 Mon Sep 17 00:00:00 2001 From: gloges Date: Wed, 25 Feb 2026 22:13:33 +0900 Subject: [PATCH 17/21] extract adjoint_isClosable_dense --- .../DDimensions/Operators/Unbounded.lean | 56 ++++++++++--------- 1 file changed, 30 insertions(+), 26 deletions(-) diff --git a/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean b/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean index ac9402d8c..7dc0276f1 100644 --- a/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean +++ b/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean @@ -107,35 +107,39 @@ section Adjoints open InnerProductSpaceSubmodule +/-- The adjoint of a densely defined, closable `LinearPMap` is densely defined. -/ +lemma adjoint_isClosable_dense (f : LinearPMap ℂ HS HS) (h_dense : Dense (f.domain : Set HS)) + (h_closable : f.IsClosable) : Dense (f†.domain : Set HS) := by + by_contra hd + have : ∃ x ∈ f†.domainᗮ, x ≠ 0 := by + apply not_forall.mp at hd + rcases hd with ⟨y, hy⟩ + have hnetop : f†.domainᗮᗮ ≠ ⊤ := by + rw [orthogonal_orthogonal_eq_closure] + exact Ne.symm (ne_of_mem_of_not_mem' trivial hy) + have hnebot : f†.domainᗮ ≠ ⊥ := by + by_contra + apply hnetop + rwa [orthogonal_eq_top_iff] + exact exists_mem_ne_zero_of_ne_bot hnebot + rcases this with ⟨x, hx, hx'⟩ + apply hx' + apply graph_fst_eq_zero_snd f.closure _ rfl + rw [← IsClosable.graph_closure_eq_closure_graph h_closable, + mem_submodule_closure_iff_mem_submoduleToLp_closure, + ← orthogonal_orthogonal_eq_closure, + ← mem_submodule_adjoint_adjoint_iff_mem_submoduleToLp_orthogonal_orthogonal, + ← LinearPMap.adjoint_graph_eq_graph_adjoint h_dense, + mem_submodule_adjoint_iff_mem_submoduleToLp_orthogonal] + rintro ⟨y, Uy⟩ hy + simp only [neg_zero, WithLp.prod_inner_apply, inner_zero_right, add_zero] + apply hx y + exact mem_domain_of_mem_graph hy + /-- The adjoint of an unbounded operator, denoted as `U†`. -/ noncomputable def adjoint : UnboundedOperator HS where toLinearPMap := U.toLinearPMap.adjoint - dense_domain := by - by_contra hd - have : ∃ x ∈ U.toLinearPMap†.domainᗮ, x ≠ 0 := by - apply not_forall.mp at hd - rcases hd with ⟨y, hy⟩ - have hnetop : U.toLinearPMap†.domainᗮᗮ ≠ ⊤ := by - rw [orthogonal_orthogonal_eq_closure] - exact Ne.symm (ne_of_mem_of_not_mem' trivial hy) - have hnebot : U.toLinearPMap†.domainᗮ ≠ ⊥ := by - by_contra - apply hnetop - rwa [orthogonal_eq_top_iff] - exact exists_mem_ne_zero_of_ne_bot hnebot - rcases this with ⟨x, hx, hx'⟩ - apply hx' - apply graph_fst_eq_zero_snd U.toLinearPMap.closure _ rfl - rw [← IsClosable.graph_closure_eq_closure_graph U.is_closable, - mem_submodule_closure_iff_mem_submoduleToLp_closure, - ← orthogonal_orthogonal_eq_closure, - ← mem_submodule_adjoint_adjoint_iff_mem_submoduleToLp_orthogonal_orthogonal, - ← LinearPMap.adjoint_graph_eq_graph_adjoint U.dense_domain, - mem_submodule_adjoint_iff_mem_submoduleToLp_orthogonal] - rintro ⟨y, Uy⟩ hy - simp only [neg_zero, WithLp.prod_inner_apply, inner_zero_right, add_zero] - apply hx y - exact mem_domain_of_mem_graph hy + dense_domain := adjoint_isClosable_dense U.toLinearPMap U.dense_domain U.is_closable is_closable := IsClosed.isClosable (adjoint_isClosed U.dense_domain) @[inherit_doc] From 7a21a2e57354bf08d94fa7173ff8fa09ba8d81a7 Mon Sep 17 00:00:00 2001 From: gloges Date: Wed, 25 Feb 2026 22:42:49 +0900 Subject: [PATCH 18/21] minor cleanup --- .../InnerProductSpace/Submodule.lean | 11 +++++------ .../DDimensions/Operators/Unbounded.lean | 18 +++++++----------- 2 files changed, 12 insertions(+), 17 deletions(-) diff --git a/PhysLean/Mathematics/InnerProductSpace/Submodule.lean b/PhysLean/Mathematics/InnerProductSpace/Submodule.lean index 2360fafae..405e83d14 100644 --- a/PhysLean/Mathematics/InnerProductSpace/Submodule.lean +++ b/PhysLean/Mathematics/InnerProductSpace/Submodule.lean @@ -37,7 +37,8 @@ def submoduleToLp : Submodule ℂ (WithLp 2 (E × E)) where lemma mem_submodule_iff_mem_submoduleToLp (f : E × E): f ∈ M ↔ (WithLp.toLp 2 f) ∈ submoduleToLp M := Eq.to_iff rfl -lemma submoduleToLp_closure : (submoduleToLp M.closure) = (submoduleToLp M).topologicalClosure := by +lemma submoduleToLp_closure : + (submoduleToLp M.topologicalClosure) = (submoduleToLp M).topologicalClosure := by rw [Submodule.ext_iff] intro x rw [← mem_submodule_iff_mem_submoduleToLp] @@ -112,10 +113,8 @@ lemma mem_submodule_adjoint_adjoint_iff_mem_submoduleToLp_orthogonal_orthogonal simp only [← mem_orthogonal] lemma mem_submodule_closure_adjoint_iff_mem_submoduleToLp_closure_orthogonal (f : E × E): - f ∈ M.closure.adjoint ↔ WithLp.toLp 2 (f.2, -f.1) ∈ (submoduleToLp M).closureᗮ := by - trans (WithLp.toLp 2 (f.2, -f.1)) ∈ (submoduleToLp M.closure)ᗮ - · apply mem_submodule_adjoint_iff_mem_submoduleToLp_orthogonal M.closure f - rw [submoduleToLp_closure] - simp [← ClosedSubmodule.mem_toSubmodule_iff] + f ∈ M.topologicalClosure.adjoint ↔ + WithLp.toLp 2 (f.2, -f.1) ∈ (submoduleToLp M).topologicalClosureᗮ := by + rw [mem_submodule_adjoint_iff_mem_submoduleToLp_orthogonal, submoduleToLp_closure] end InnerProductSpaceSubmodule diff --git a/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean b/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean index 7dc0276f1..7a4aeea48 100644 --- a/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean +++ b/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean @@ -133,8 +133,7 @@ lemma adjoint_isClosable_dense (f : LinearPMap ℂ HS HS) (h_dense : Dense (f.do mem_submodule_adjoint_iff_mem_submoduleToLp_orthogonal] rintro ⟨y, Uy⟩ hy simp only [neg_zero, WithLp.prod_inner_apply, inner_zero_right, add_zero] - apply hx y - exact mem_domain_of_mem_graph hy + exact hx y (mem_domain_of_mem_graph hy) /-- The adjoint of an unbounded operator, denoted as `U†`. -/ noncomputable def adjoint : UnboundedOperator HS where @@ -154,8 +153,8 @@ lemma adjoint_toLinearPMap : U†.toLinearPMap = U.toLinearPMap† := rfl lemma isSelfAdjoint_def : IsSelfAdjoint U ↔ U† = U := Iff.rfl lemma isSelfAdjoint_iff : IsSelfAdjoint U ↔ IsSelfAdjoint U.toLinearPMap := by - rw [isSelfAdjoint_def, LinearPMap.isSelfAdjoint_def, ← adjoint_toLinearPMap] - exact UnboundedOperator.ext_iff' U† U + rw [isSelfAdjoint_def, LinearPMap.isSelfAdjoint_def, ← adjoint_toLinearPMap, + UnboundedOperator.ext_iff'] lemma adjoint_isClosed : (U†).IsClosed := LinearPMap.adjoint_isClosed U.dense_domain @@ -168,10 +167,8 @@ lemma closure_adjoint_eq_adjoint : U.closure† = U† := by rw [closure_toLinearPMap, ← IsClosable.graph_closure_eq_closure_graph U.is_closable] ext f - trans WithLp.toLp 2 (f.2, -f.1) ∈ (submoduleToLp U.toLinearPMap.graph).topologicalClosureᗮ - · exact mem_submodule_closure_adjoint_iff_mem_submoduleToLp_closure_orthogonal _ _ - rw [orthogonal_closure] - exact Iff.symm (mem_submodule_adjoint_iff_mem_submoduleToLp_orthogonal _ _) + rw [mem_submodule_closure_adjoint_iff_mem_submoduleToLp_closure_orthogonal, + orthogonal_closure, mem_submodule_adjoint_iff_mem_submoduleToLp_orthogonal] lemma adjoint_adjoint_eq_closure : U†† = U.closure := by -- Reduce to statement about graphs using density and closability assumptions @@ -182,9 +179,8 @@ lemma adjoint_adjoint_eq_closure : U†† = U.closure := by rw [closure_toLinearPMap, ← IsClosable.graph_closure_eq_closure_graph U.is_closable] ext f - trans WithLp.toLp 2 f ∈ (submoduleToLp U.toLinearPMap.graph)ᗮᗮ - · exact mem_submodule_adjoint_adjoint_iff_mem_submoduleToLp_orthogonal_orthogonal _ _ - rw [orthogonal_orthogonal_eq_closure, mem_submodule_closure_iff_mem_submoduleToLp_closure] + rw [mem_submodule_adjoint_adjoint_iff_mem_submoduleToLp_orthogonal_orthogonal, + orthogonal_orthogonal_eq_closure, mem_submodule_closure_iff_mem_submoduleToLp_closure] end Adjoints From 3c311090157808b9a8645c8b2cc6ec91f9d0eb40 Mon Sep 17 00:00:00 2001 From: gloges Date: Wed, 25 Feb 2026 23:16:05 +0900 Subject: [PATCH 19/21] lint fixes --- PhysLean/Mathematics/InnerProductSpace/Submodule.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/PhysLean/Mathematics/InnerProductSpace/Submodule.lean b/PhysLean/Mathematics/InnerProductSpace/Submodule.lean index 405e83d14..452258608 100644 --- a/PhysLean/Mathematics/InnerProductSpace/Submodule.lean +++ b/PhysLean/Mathematics/InnerProductSpace/Submodule.lean @@ -34,7 +34,7 @@ def submoduleToLp : Submodule ℂ (WithLp 2 (E × E)) where intro c x hx exact Submodule.smul_mem M c hx -lemma mem_submodule_iff_mem_submoduleToLp (f : E × E): +lemma mem_submodule_iff_mem_submoduleToLp (f : E × E) : f ∈ M ↔ (WithLp.toLp 2 f) ∈ submoduleToLp M := Eq.to_iff rfl lemma submoduleToLp_closure : @@ -67,7 +67,7 @@ lemma submoduleToLp_closure : use w.ofLp exact ⟨Set.mem_preimage.mp (ht1 (ht2' w hw.1)), (mem_toAddSubgroup (submoduleToLp M)).mp hw.2⟩ -lemma mem_submodule_closure_iff_mem_submoduleToLp_closure (f : E × E): +lemma mem_submodule_closure_iff_mem_submoduleToLp_closure (f : E × E) : f ∈ M.topologicalClosure ↔ (WithLp.toLp 2 f) ∈ (submoduleToLp M).topologicalClosure := by rw [← submoduleToLp_closure] rfl @@ -112,7 +112,7 @@ lemma mem_submodule_adjoint_adjoint_iff_mem_submoduleToLp_orthogonal_orthogonal simp [hw'] simp only [← mem_orthogonal] -lemma mem_submodule_closure_adjoint_iff_mem_submoduleToLp_closure_orthogonal (f : E × E): +lemma mem_submodule_closure_adjoint_iff_mem_submoduleToLp_closure_orthogonal (f : E × E) : f ∈ M.topologicalClosure.adjoint ↔ WithLp.toLp 2 (f.2, -f.1) ∈ (submoduleToLp M).topologicalClosureᗮ := by rw [mem_submodule_adjoint_iff_mem_submoduleToLp_orthogonal, submoduleToLp_closure] From a318c06089111a08ce7d41364ec8a40b2fc4b7bd Mon Sep 17 00:00:00 2001 From: Daniel Morrison <39346894+morrison-daniel@users.noreply.github.com> Date: Fri, 27 Feb 2026 15:43:52 -0800 Subject: [PATCH 20/21] Remove extra blank lines --- PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean b/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean index 7a4aeea48..aaae63111 100644 --- a/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean +++ b/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean @@ -165,7 +165,6 @@ lemma closure_adjoint_eq_adjoint : U.closure† = U† := by rw [adjoint_toLinearPMap, adjoint_graph_eq_graph_adjoint U.closure.dense_domain] rw [adjoint_toLinearPMap, adjoint_graph_eq_graph_adjoint U.dense_domain] rw [closure_toLinearPMap, ← IsClosable.graph_closure_eq_closure_graph U.is_closable] - ext f rw [mem_submodule_closure_adjoint_iff_mem_submoduleToLp_closure_orthogonal, orthogonal_closure, mem_submodule_adjoint_iff_mem_submoduleToLp_orthogonal] @@ -177,7 +176,6 @@ lemma adjoint_adjoint_eq_closure : U†† = U.closure := by rw [adjoint_toLinearPMap, adjoint_graph_eq_graph_adjoint U†.dense_domain] rw [adjoint_toLinearPMap, adjoint_graph_eq_graph_adjoint U.dense_domain] rw [closure_toLinearPMap, ← IsClosable.graph_closure_eq_closure_graph U.is_closable] - ext f rw [mem_submodule_adjoint_adjoint_iff_mem_submoduleToLp_orthogonal_orthogonal, orthogonal_orthogonal_eq_closure, mem_submodule_closure_iff_mem_submoduleToLp_closure] From b27f745f4cd51fc09c94c7537bc4336911a4639a Mon Sep 17 00:00:00 2001 From: Daniel Morrison <39346894+morrison-daniel@users.noreply.github.com> Date: Fri, 27 Feb 2026 15:45:19 -0800 Subject: [PATCH 21/21] Remove extra blank lines --- .../QuantumMechanics/DDimensions/SpaceDHilbertSpace/Basic.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/PhysLean/QuantumMechanics/DDimensions/SpaceDHilbertSpace/Basic.lean b/PhysLean/QuantumMechanics/DDimensions/SpaceDHilbertSpace/Basic.lean index 0e0ec1ac0..5aeb42810 100644 --- a/PhysLean/QuantumMechanics/DDimensions/SpaceDHilbertSpace/Basic.lean +++ b/PhysLean/QuantumMechanics/DDimensions/SpaceDHilbertSpace/Basic.lean @@ -124,11 +124,9 @@ lemma eLpNorm_mk {f : Space d → ℂ} {hf : MemHS f} : eLpNorm (mk hf) 2 = eLpN lemma mem_iff {f : Space d → ℂ} (hf : AEStronglyMeasurable f volume) : AEEqFun.mk f hf ∈ SpaceDHilbertSpace d ↔ Integrable (fun x ↦ ‖f x‖ ^ 2) := by rw [Lp.mem_Lp_iff_memLp, MemLp, eLpNorm_aeeqFun] - have h1 := AEEqFun.aestronglyMeasurable (AEEqFun.mk f hf) have h2 : AEStronglyMeasurable (fun x ↦ norm (f x) ^ 2) := AEStronglyMeasurable.pow (continuous_norm.comp_aestronglyMeasurable hf) 2 - simp only [h1] simp only [eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top (NeZero.ne' 2).symm (ENNReal.top_ne_ofNat).symm, ENNReal.toReal_ofNat, ENNReal.rpow_ofNat]