diff --git a/Physlib.lean b/Physlib.lean index f12b50657..f9490fb5d 100644 --- a/Physlib.lean +++ b/Physlib.lean @@ -86,6 +86,7 @@ public import Physlib.Mathematics.InnerProductSpace.Calculus public import Physlib.Mathematics.InnerProductSpace.Submodule public import Physlib.Mathematics.KroneckerDelta public import Physlib.Mathematics.LinearMaps +public import Physlib.Mathematics.LinearPMap public import Physlib.Mathematics.List public import Physlib.Mathematics.List.InsertIdx public import Physlib.Mathematics.List.InsertionSort diff --git a/Physlib/Mathematics/LinearPMap.lean b/Physlib/Mathematics/LinearPMap.lean new file mode 100644 index 000000000..eee6b16c1 --- /dev/null +++ b/Physlib/Mathematics/LinearPMap.lean @@ -0,0 +1,368 @@ +/- +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 +-/ +module + +public import Mathlib.Analysis.InnerProductSpace.LinearPMap +/-! + +# LinearPMap + +## i. Overview + +In this module we collect some basic results about `LinearPMap`s. + +Most important is the definition of restricted composition. +The composition of two partial linear maps `g : F →ₗ.[R] G` and `f : E →ₗ.[R] F` is defined +only if the range of `f` is contained in the domain of `g` (c.f. `LinearPMap.comp`). +`g.compRestricted f` (`g ∘ᵣ f`) is defined to be the composition of `g` with the restriction of `f` +to exactly those `x : f.domain` for which `f x ∈ g.domain`. This allows one to work with the +composition of partial linear maps while having the domain implicitly accounted for. + +## ii. Key results + +- `LinearPMap.sum` : The finite sum of partial linear maps. +- `LinearPMap.compRestricted` (`∘ᵣ`) : For two partial linear maps + `g : F →ₗ[R] G` and `f : E →ₗ[R] F`, the composition of `g` with `f` + with natural domain `{x : f.domain | f x ∈ g.domain}`. +- `LinearPMap.instMonoid` : Partial linear maps `E →ₗ.[R] E` with `compRestricted` + for multiplication and the identity map for `1` comprise a monoid. + +## iii. Table of contents + +- A. Inequalities +- B. Finite sums +- C. Restricted composition +- D. Monoid +- E. Inverses + +## iv. References + +-/ + +@[expose] public section + +namespace LinearPMap + +open Submodule + +variable {R : Type*} [Ring R] +variable {E : Type*} [AddCommGroup E] [Module R E] +variable {F : Type*} [AddCommGroup F] [Module R F] + +/-! +## A. Inequalities +-/ + +section Inequalities + +variable (f f₁ f₂ f₃ : E →ₗ.[R] F) {g g₁ g₂ : E →ₗ.[R] F} + +lemma sub_le_zero : f - f ≤ 0 := ⟨le_top, by simp [sub_apply]⟩ + +lemma neg_add_le_zero : -f + f ≤ 0 := ⟨le_top, by simp [add_apply]⟩ + +lemma le_iff_neg_le_neg : g₁ ≤ g₂ ↔ -g₁ ≤ -g₂ := + ⟨fun ⟨h, h'⟩ ↦ ⟨h, fun _ _ h'' ↦ by simp [h' h'']⟩, fun ⟨h, _⟩ ↦ ⟨h, fun _ _ _ ↦ by aesop⟩⟩ + +lemma le_neg_iff_neg_le : g₁ ≤ -g₂ ↔ -g₁ ≤ g₂ := by rw [le_iff_neg_le_neg, neg_neg] + +lemma add_sub_le_cancel : f₁ + (f₂ - f₁) ≤ f₂ := + ⟨by simp [add_domain, sub_domain], fun _ _ h ↦ by simp [add_apply, sub_apply, h]⟩ + +lemma add_sub_le_cancel_left : f₁ + f₂ - f₁ ≤ f₂ := add_sub_assoc f₁ f₂ f₁ ▸ add_sub_le_cancel f₁ f₂ + +lemma add_sub_le_cancel_right : f₁ + f₂ - f₂ ≤ f₁ := add_comm f₁ f₂ ▸ add_sub_le_cancel_left f₂ f₁ + +lemma add_add_sub_le_cancel : f₁ + f₂ + (f₃ - f₂) ≤ f₁ + f₃ := + ⟨fun _ _ ↦ by simp_all [add_domain, sub_domain], fun _ _ h ↦ by simp [add_apply, sub_apply, h]⟩ + +lemma add_sub_sub_le_cancel : f₁ + f₂ - (f₁ - f₃) ≤ f₂ + f₃ := + ⟨fun _ _ ↦ by simp_all [add_domain, sub_domain], fun _ _ h ↦ by simp [add_apply, sub_apply, h]⟩ + +lemma sub_sub_sub_le_cancel_right : f₁ - f₂ - (f₃ - f₂) ≤ f₁ - f₃ := by + simp only [sub_eq_add_neg, neg_add] + exact sub_eq_add_neg (-f₃) (-f₂) ▸ add_add_sub_le_cancel f₁ (-f₂) (-f₃) + +lemma sub_sub_sub_le_cancel_left : f₁ - f₂ - (f₁ - f₃) ≤ f₃ - f₂ := + sub_eq_add_neg f₁ f₂ ▸ neg_add_eq_sub f₂ f₃ ▸ add_sub_sub_le_cancel f₁ (-f₂) f₃ + +lemma sub_le_of_le_add (h : g ≤ g₁ + g₂) : g - g₂ ≤ g₁ := by + constructor + · exact (inf_le_of_left_le le_rfl).trans (le_inf_iff.mp <| add_domain g₁ g₂ ▸ h.1).1 + · intro ⟨x, hx⟩ ⟨y, hy⟩ rfl + simp [sub_apply, @h.2 ⟨x, hx.1⟩ ⟨x, ⟨hy, hx.2⟩⟩ rfl, add_apply] + +lemma sub_add_le_cancel : f₁ - f₂ + f₂ ≤ f₁ := + sub_eq_add_neg f₁ f₂ ▸ sub_neg_eq_add _ f₂ ▸ add_sub_le_cancel_right f₁ (-f₂) + +lemma add_le_of_le_sub (h : g ≤ g₁ - g₂) : g + g₂ ≤ g₁ := + sub_neg_eq_add g g₂ ▸ sub_le_of_le_add (sub_eq_add_neg g₁ g₂ ▸ h) + +lemma add_left_le_of_le (h : g₁ ≤ g₂) : f + g₁ ≤ f + g₂ := by + constructor + · simp only [add_domain, le_inf_iff, inf_le_left, true_and] + exact (inf_le_of_right_le le_rfl).trans h.1 + · intro x y hxy + simp_rw [add_apply, @h.2 ⟨x, x.2.2⟩ ⟨y, y.2.2⟩ hxy, hxy] + +lemma add_right_le_of_le (h : g₁ ≤ g₂) : g₁ + f ≤ g₂ + f := + add_comm f g₁ ▸ add_comm f g₂ ▸ add_left_le_of_le f h + +lemma sub_right_le_of_le (h : g₁ ≤ g₂) : g₁ - f ≤ g₂ - f := + sub_eq_add_neg g₁ f ▸ sub_eq_add_neg g₂ f ▸ add_right_le_of_le (-f) h + +lemma sub_left_le_of_le (h : g₁ ≤ g₂) : f - g₁ ≤ f - g₂ := + neg_sub g₁ f ▸ neg_sub g₂ f ▸ le_iff_neg_le_neg.mp (sub_right_le_of_le f h) + +end Inequalities + +/-! +## B. Finite sums +-/ + +section Sums + +variable {α : Type*} [Fintype α] (f : α → E →ₗ.[R] F) + +/-- A finite sum of partial linear maps. + + `sum f` and `∑ a, f a` are equal, but not by definition. + With `sum f` both `domain` and `toFun` are made explicit. -/ +def sum : E →ₗ.[R] F where + domain := ⨅ a, (f a).domain + toFun := ∑ a, (f a).toFun ∘ₗ inclusion (fun _ _ ↦ by simp_all only [mem_iInf]) + +lemma sum_domain : (sum f).domain = ⨅ a, (f a).domain := rfl + +lemma sum_domain_le (a : α) : (sum f).domain ≤ (f a).domain := fun _ _ ↦ by simp_all [sum, mem_iInf] + +@[simp] +lemma sum_apply (ψ : (sum f).domain) : sum f ψ = ∑ a, f a ⟨ψ, sum_domain_le f a ψ.2⟩ := by + simp [sum, inclusion_apply] + +end Sums + +/-! +## C. Restricted composition +-/ + +section Composition + +variable {G : Type*} [AddCommGroup G] [Module R G] +variable (g g₁ g₂ : F →ₗ.[R] G) (f f₁ f₂ : E →ₗ.[R] F) +variable {v : F →ₗ.[R] G} {u : E →ₗ.[R] F} + +/-- `g ∘ᵣ f` is the composition of `g` with `f` restricted to a domain consisting of exactly those + `x : f.domain` for which `f x ∈ g.domain`. -/ +def compRestricted : E →ₗ.[R] G := + g.comp (f.domRestrict <| (g.domain.comap f.toFun).map f.domain.subtype) (by + intro ⟨x, h, _⟩ + simp only [map_coe, subtype_apply, comap_coe, Set.mem_image, Set.mem_preimage, + toFun_eq_coe, SetLike.mem_coe] at h + obtain ⟨y, hy, hy'⟩ := h + rw [domRestrict_apply hy'.symm] + exact hy) + +@[inherit_doc compRestricted] +infixr:80 " ∘ᵣ " => compRestricted + +lemma compRestricted_domain_le : (g ∘ᵣ f).domain ≤ f.domain := fun _ h ↦ h.2 + +lemma compRestricted_domain : (g ∘ᵣ f).domain = (g.domain.comap f.toFun).map f.domain.subtype := by + change (f.domRestrict <| (g.domain.comap f.toFun).map f.domain.subtype).domain = _ + rw [domRestrict_domain] + refine inf_of_le_left ?_ + intro x h + simp only [mem_map, mem_comap, toFun_eq_coe, subtype_apply, Subtype.exists, exists_and_right, + exists_eq_right] at h + exact h.choose + +lemma mem_compRestricted_domain_iff {x : E} : + x ∈ (v ∘ᵣ u).domain ↔ ∃ h : x ∈ u.domain, u ⟨x, h⟩ ∈ v.domain := by + simp [compRestricted_domain] + +lemma mem_compRestricted_domain_iff' {x : E} : + x ∈ (v ∘ᵣ u).domain ↔ ∃ y : u.domain, x = y ∧ ∃ y' : v.domain, u y = y' := by + simp [mem_compRestricted_domain_iff] + +lemma mem_domain_of_mem_compRestricted_domain (x : (v ∘ᵣ u).domain) : u ⟨x, x.2.2⟩ ∈ v.domain := + (mem_compRestricted_domain_iff.mp x.2).choose_spec + +@[simp] +lemma compRestricted_apply (x : (v ∘ᵣ u).domain) : + (v ∘ᵣ u) x = v ⟨u ⟨x, x.2.2⟩, mem_domain_of_mem_compRestricted_domain x⟩ := rfl + +/-- The zero map is right-absorbing. -/ +@[simp] +lemma compRestricted_zero : g ∘ᵣ (0 : E →ₗ.[R] F) = 0 := by + ext + · simp [mem_compRestricted_domain_iff] + · exact g.map_zero + +lemma compRestricted_assoc {H : Type*} [AddCommGroup H] [Module R H] + (f₁ : G →ₗ.[R] H) (f₂ : F →ₗ.[R] G) (f₃ : E →ₗ.[R] F) : + (f₁ ∘ᵣ f₂) ∘ᵣ f₃ = f₁ ∘ᵣ f₂ ∘ᵣ f₃ := by + ext + · simp only [mem_compRestricted_domain_iff] + tauto + · rfl + +/-- `compRestricted` is the same as `comp` when the range of `u` is contained in `v.domain`. -/ +lemma compRestricted_eq_comp (h : ∀ x : u.domain, u x ∈ v.domain) : + v ∘ᵣ u = v.comp u h := by + ext x + · change _ ↔ x ∈ u.domain + simp [mem_compRestricted_domain_iff, h] + · rfl + +/-- `compRestricted` is maximal amongst compositions of `v` with domain restrictions of `u`. -/ +lemma comp_le_compRestricted + {S : Submodule R E} (h : ∀ x : (u.domRestrict S).domain, u ⟨x, x.2.2⟩ ∈ v.domain) : + v.comp (u.domRestrict S) h ≤ v ∘ᵣ u := + ⟨fun x hx ↦ mem_compRestricted_domain_iff.mpr ⟨hx.2, h ⟨x, hx⟩⟩, by aesop⟩ + +lemma compRestricted_mono_left {g g' : F →ₗ.[R] G} (h : g ≤ g') (f : E →ₗ.[R] F) : + g ∘ᵣ f ≤ g' ∘ᵣ f := by + constructor + · intro x hx + obtain ⟨hx', hfx⟩ := mem_compRestricted_domain_iff.mp hx + exact mem_compRestricted_domain_iff.mpr ⟨hx', h.1 hfx⟩ + · intro x y hxy + exact @h.2 ⟨f ⟨x, x.2.2⟩, mem_domain_of_mem_compRestricted_domain x⟩ + ⟨f ⟨y, y.2.2⟩, mem_domain_of_mem_compRestricted_domain y⟩ (by simp [hxy]) + +lemma compRestricted_mono_right (g : F →ₗ.[R] G) {f f' : E →ₗ.[R] F} (h : f ≤ f') : + g ∘ᵣ f ≤ g ∘ᵣ f' := by + constructor + · intro x hx + obtain ⟨hx', hfx⟩ := mem_compRestricted_domain_iff.mp hx + exact mem_compRestricted_domain_iff.mpr ⟨h.1 hx', (@h.2 ⟨x, hx'⟩ ⟨x, h.1 hx'⟩ rfl) ▸ hfx⟩ + · intro x y hxy + simp only [compRestricted_apply, @h.2 ⟨x, x.2.2⟩ ⟨y, y.2.2⟩ hxy] + +@[simp] +lemma neg_compRestricted : (-g) ∘ᵣ f = -g ∘ᵣ f := rfl + +@[simp] +lemma compRestricted_neg : g ∘ᵣ (-f) = -g ∘ᵣ f := by + ext x hx hx' + · simp [mem_compRestricted_domain_iff] + · obtain ⟨h, h'⟩ := mem_compRestricted_domain_iff.mp (neg_domain (g ∘ᵣ f) ▸ hx') + exact g.toFun.map_neg ⟨f ⟨x, h⟩, h'⟩ + +lemma add_compRestricted : (g₁ + g₂) ∘ᵣ f = g₁ ∘ᵣ f + g₂ ∘ᵣ f := by + ext x hx hx' + · simp only [mem_compRestricted_domain_iff, add_domain, mem_inf] + tauto + · simp [add_apply] + +lemma sub_compRestricted : (g₁ - g₂) ∘ᵣ f = g₁ ∘ᵣ f - g₂ ∘ᵣ f := by + simp [sub_eq_add_neg, add_compRestricted] + +lemma compRestricted_add_ge : g ∘ᵣ f₁ + g ∘ᵣ f₂ ≤ g ∘ᵣ (f₁ + f₂) := by + constructor + · intro x hx + obtain ⟨h₁, h₁'⟩ := mem_compRestricted_domain_iff.mp hx.1 + obtain ⟨h₂, h₂'⟩ := mem_compRestricted_domain_iff.mp hx.2 + exact mem_compRestricted_domain_iff.mpr ⟨⟨h₁, h₂⟩, add_mem h₁' h₂'⟩ + · intro x y hxy + obtain ⟨h₁, h₁'⟩ := mem_compRestricted_domain_iff.mp x.2.1 + obtain ⟨h₂, h₂'⟩ := mem_compRestricted_domain_iff.mp x.2.2 + simp [← hxy, add_apply, ← g.map_add ⟨f₁ ⟨x, h₁⟩, h₁'⟩ ⟨f₂ ⟨x, h₂⟩, h₂'⟩] + +lemma compRestricted_sub_ge : g ∘ᵣ f₁ - g ∘ᵣ f₂ ≤ g ∘ᵣ (f₁ - f₂) := by + simp only [sub_eq_add_neg, ← compRestricted_neg] + exact compRestricted_add_ge g f₁ (-f₂) + +lemma compRestricted_smul {S : Type*} [DivisionRing S] + [Module S E] [Module S F] [Module S G] [SMulCommClass S S F] [SMulCommClass S S G] + {c : S} (hc : c ≠ 0) (g : F →ₗ.[S] G) (f : E →ₗ.[S] F) : + g ∘ᵣ (c • f) = c • (g ∘ᵣ f) := by + ext x hx hx' + · simp [mem_compRestricted_domain_iff, g.domain.smul_mem_iff hc] + · obtain ⟨h, h'⟩ := mem_compRestricted_domain_iff.mp (smul_domain c (g ∘ᵣ f) ▸ hx') + exact g.toFun.map_smul c ⟨f ⟨x, h⟩, h'⟩ + +@[simp] +lemma smul_compRestricted {M : Type*} [Monoid M] [DistribMulAction M G] [SMulCommClass R M G] + (c : M) (g : F →ₗ.[R] G) (f : E →ₗ.[R] F) : + (c • g) ∘ᵣ f = c • (g ∘ᵣ f) := by + ext + · simp [compRestricted_domain] + · simp + +end Composition + +/-! +## D. Monoid + +Partial linear maps `E →ₗ.[R] E` with `compRestricted` for multiplication and +the identity map (domain `⊤`) for `1` comprise a monoid. +-/ + +section Monoid + +instance instMonoid : Monoid (E →ₗ.[R] E) where + mul := compRestricted + mul_assoc := compRestricted_assoc + one := ⟨⊤, topEquiv.toLinearMap⟩ + one_mul f := by + change ⟨⊤, topEquiv.toLinearMap⟩ ∘ᵣ f = f + ext + · simp [mem_compRestricted_domain_iff] + · rfl + mul_one f := by + change f ∘ᵣ ⟨⊤, topEquiv.toLinearMap⟩ = f + ext + · simp [mem_compRestricted_domain_iff] + · rfl + +lemma mul_def (f₁ f₂ : E →ₗ.[R] E) : f₁ * f₂ = f₁ ∘ᵣ f₂ := rfl + +@[simp] +lemma one_domain : (1 : E →ₗ.[R] E).domain = ⊤ := rfl + +@[simp] +lemma one_toFun : (1 : E →ₗ.[R] E).toFun = topEquiv.toLinearMap := rfl + +@[simp] +lemma one_coe : (1 : E →ₗ.[R] E).toFun' = ⇑topEquiv.toLinearMap := rfl + +end Monoid + +/-! +## E. Inverses +-/ + +section Inverses + +variable {f : E →ₗ.[R] F} (h_ker : f.toFun.ker = ⊥) +include h_ker + +lemma inverse_ker : f.inverse.toFun.ker = ⊥ := by + refine LinearMap.ker_eq_bot'.mpr fun ⟨y, hy⟩ hy' ↦ ?_ + obtain ⟨x, hx⟩ := inverse_domain (f := f) ▸ hy + simp_all [inverse_apply_eq (x := x) (y := ⟨y, hy⟩) h_ker hx] + +lemma inverse_inverse : f.inverse.inverse = f := by + ext x hx hx' + · rw [inverse_domain, inverse_range h_ker] + · refine inverse_apply_eq (y := ⟨x, hx⟩) (x := ⟨f ⟨x, hx'⟩, by simp [inverse_domain]⟩) ?_ ?_ + · exact inverse_ker h_ker + · exact inverse_apply_eq (y := ⟨f ⟨x, hx'⟩, by simp [inverse_domain]⟩) (x := ⟨x, hx'⟩) h_ker rfl + +lemma inverse_compRestricted_eq : f.inverse ∘ᵣ f = domRestrict 1 f.domain := by + ext x hx hx' + · simp [mem_compRestricted_domain_iff, inverse_domain, ← toFun_eq_coe] + · exact inverse_apply_eq (x := ⟨x, hx.2⟩) h_ker rfl + +lemma compRestricted_inverse_eq : f ∘ᵣ f.inverse = domRestrict 1 f.inverse.domain := by + nth_rw 1 [← inverse_inverse h_ker] + exact inverse_compRestricted_eq (inverse_ker h_ker) + +end Inverses + +end LinearPMap diff --git a/Physlib/QuantumMechanics/DDimensions/Operators/Unbounded.lean b/Physlib/QuantumMechanics/DDimensions/Operators/Unbounded.lean index 76842c481..b6e9fec6e 100644 --- a/Physlib/QuantumMechanics/DDimensions/Operators/Unbounded.lean +++ b/Physlib/QuantumMechanics/DDimensions/Operators/Unbounded.lean @@ -6,17 +6,22 @@ Authors: Gregory J. Loges module public import Physlib.Mathematics.InnerProductSpace.Submodule +public import Physlib.Mathematics.LinearPMap /-! # Unbounded operators ## i. Overview -In this module we introduce unbounded operators on inner product spaces. By "unbounded operator" -we mean a partially-defined linear map (`LinearPMap`) which is both densely defined and closable. -These provide the mathematical structure appropriate for describing operators in non-relativistic -quantum mechanics. Of particular interest are (essentially) self-adjoint unbounded operators since -these correspond to physical observables. +The appropriate mathematical objects for discussing operators in non-relativistic quantum mechanics +are partially-defined linear map (`LinearPMap`) between complex Hilbert spaces, `H →ₗ.[ℂ] H'`. +An import class of operators in NRQM are those which are both densely defined and closable, +which we refer to as _unbounded_. When `H = H'` operators may also be symmetric, self-adjoint or +essentially self-adjoint (closure is self-adjoint). + +In this module we collect results on how the properties `HasDenseDomain`, `IsUnbounded`, +`IsSymmetric`, `IsSelfAdjoint` and `IsEssentiallySelfAdjoint` interact with the basic algebraic +operations, closure, adjoints and each other. ### Notes @@ -33,10 +38,15 @@ these correspond to physical observables. ## ii. Key results -- `LinearPMap.compRestricted` : For two partial linear maps `g : F →ₗ[R] G` and `f : E →ₗ[R] F`, - the composition of `g` with `f` with natural domain `{x : f.domain | f x ∈ g.domain}`. -- `LinearPMap.instMonoid` : Partial linear maps `E →ₗ.[R] E` with `compRestricted` - for multiplication and the identity map for `1` comprise a monoid. +Definitions +- `HasDenseDomain` : An operator `U : H →ₗ.[ℂ] H'` has dense domain if `U.domain` is dense in `H`. +- `IsUnbounded` : An operator is unbounded if it is both densely defined and closable. +- `IsSymmetric` : An operator `T : H →ₗ.[ℂ] H` is symmetric if `⟪T x, y⟫_ℂ = ⟪x, T y⟫_ℂ` holds + for all `x y : T.domain`. +- `IsEssentiallySelfAdjoint` : An operator `T : H →ₗ.[ℂ] H` is essentially self-adjoint if + its closure is self-adjoint. + +Results - `adjoint_add_le_add_adjoint` : The inequality `U₁† + U₂† ≤ (U₁ + U₂)†` when `U₁ + U₂` has dense domain. - `adjoint_compRestricted_le_compRestricted_adjoint` : The inequality `U† ∘ᵣ V† ≤ (V ∘ᵣ U)†` @@ -50,32 +60,22 @@ these correspond to physical observables. ## iii. Table of contents -- A. General - - A.1. DistribMulAction - - A.2. Finite sums - - A.3. Restricted composition - - A.4. Monoid - - A.5. Inequalities - - A.6. Inverses -- B. Operators on inner product/Hilbert spaces - - B.1. Definitions - - B.2. Basic properties - - B.2.1. Dense domain - - B.2.2. Closability - - B.2.3. Adjoints - - B.2.4. Continuity / boundedness - - B.3. Classes of operators - - B.3.1. Symmetric operators - - B.3.2. Self-adjoint operators - - B.3.3. Essentially self-adjoint operators - - B.3.4. Unbounded operators +- A. Definitions +- B. Basic properties + - B.1. Dense domain + - B.2. Closability + - B.3. Adjoints + - B.4. Continuity / boundedness +- C. Classes of operators + - C.1. Symmetric operators + - C.2. Self-adjoint operators + - C.3. Essentially self-adjoint operators + - C.4. Unbounded operators ## iv. References -- M. Reed & B. Simon, (1972). "Methods of modern mathematical physics: Vol. 1. Functional analysis". - Academic Press. https://doi.org/10.1016/B978-0-12-585001-8.X5001-6 -- K. Schmüdgen, (2012). "Unbounded self-adjoint operators on Hilbert space" (Vol. 265). Springer. - https://doi.org/10.1007/978-94-007-4753-1 +- [Reed and Simon, *Methods of Modern Mathematical Physics, Vol. I: Functional Analysis*][Reed1972] +- [Konrad Schmüdgen, *Unbounded Self-Adjoint Operators on Hilbert Space*][Schmudgen2012] -/ @@ -83,360 +83,6 @@ these correspond to physical observables. namespace LinearPMap -/-! -## A. General - -This section contains useful general results for partial linear maps which do not rely -on an inner product/Hilbert space structure. --/ - -section General - -open Submodule - -variable {R : Type*} [Ring R] -variable {E : Type*} [AddCommGroup E] [Module R E] -variable {F : Type*} [AddCommGroup F] [Module R F] - -/-! -### A.1. DistribMulAction --/ - -section - -variable {M : Type*} [Monoid M] [DistribMulAction M F] [SMulCommClass R M F] - -instance instDistribMulAction : DistribMulAction M (E →ₗ.[R] F) where - smul_zero _ := by ext; rfl; simp - smul_add _ _ _ := by ext; rfl; simp [add_apply] - -end - -/-! -### A.2. Finite sums --/ - -section - -variable {α : Type*} [Fintype α] (f : α → E →ₗ.[R] F) - -/-- A finite sum of partial linear maps. - - `sum f` and `∑ a, f a` are equal, but not by definition. - With `sum f` both `domain` and `toFun` are made explicit. -/ -def sum : E →ₗ.[R] F where - domain := ⨅ a, (f a).domain - toFun := ∑ a, (f a).toFun ∘ₗ inclusion (fun _ _ ↦ by simp_all only [mem_iInf]) - -lemma sum_domain : (sum f).domain = ⨅ a, (f a).domain := rfl - -lemma sum_domain_le (a : α) : (sum f).domain ≤ (f a).domain := fun _ _ ↦ by simp_all [sum, mem_iInf] - -@[simp] -lemma sum_apply (ψ : (sum f).domain) : sum f ψ = ∑ a, f a ⟨ψ, sum_domain_le f a ψ.2⟩ := by - simp [sum, inclusion_apply] - -end - -/-! -### A.3. Restricted composition - -The composition of two partial linear maps `g : F →ₗ.[R] G` and `f : E →ₗ.[R] F` is defined -only if the range of `f` is contained in the domain of `g` (c.f. `LinearPMap.comp`). -`g.compRestricted f` (`g ∘ᵣ f`) is defined to be the composition of `g` with the restriction of `f` -to exactly those `x : f.domain` for which `f x ∈ g.domain`. This allows one to work with the -composition of partial linear maps while having the domain implicitly accounted for. --/ - -section - -variable {G : Type*} [AddCommGroup G] [Module R G] - -/-- `g ∘ᵣ f` is the composition of `g` with `f` restricted to a domain consisting of exactly those - `x : f.domain` for which `f x ∈ g.domain`. -/ -def compRestricted (g : F →ₗ.[R] G) (f : E →ₗ.[R] F) : E →ₗ.[R] G := - g.comp (f.domRestrict <| (g.domain.comap f.toFun).map f.domain.subtype) (by - intro ⟨x, h, _⟩ - simp only [map_coe, subtype_apply, comap_coe, Set.mem_image, Set.mem_preimage, - toFun_eq_coe, SetLike.mem_coe] at h - obtain ⟨y, hy, hy'⟩ := h - rw [domRestrict_apply hy'.symm] - exact hy) - -@[inherit_doc compRestricted] -infixr:80 " ∘ᵣ " => compRestricted - -lemma compRestricted_domain_le (g : F →ₗ.[R] G) (f : E →ₗ.[R] F) : (g ∘ᵣ f).domain ≤ f.domain := - fun _ h ↦ h.2 - -lemma compRestricted_domain (g : F →ₗ.[R] G) (f : E →ₗ.[R] F) : - (g ∘ᵣ f).domain = (g.domain.comap f.toFun).map f.domain.subtype := by - change (f.domRestrict <| (g.domain.comap f.toFun).map f.domain.subtype).domain = _ - rw [domRestrict_domain] - refine inf_of_le_left ?_ - intro x h - simp only [mem_map, mem_comap, toFun_eq_coe, subtype_apply, Subtype.exists, exists_and_right, - exists_eq_right] at h - exact h.choose - -lemma mem_compRestricted_domain_iff {g : F →ₗ.[R] G} {f : E →ₗ.[R] F} {x : E} : - x ∈ (g ∘ᵣ f).domain ↔ ∃ h : x ∈ f.domain, f ⟨x, h⟩ ∈ g.domain := by - simp [compRestricted_domain] - -lemma mem_compRestricted_domain_iff' {g : F →ₗ.[R] G} {f : E →ₗ.[R] F} {x : E} : - x ∈ (g ∘ᵣ f).domain ↔ ∃ y : f.domain, x = y ∧ ∃ y' : g.domain, f y = y' := by - simp [mem_compRestricted_domain_iff] - -lemma mem_domain_of_mem_compRestricted_domain - {g : F →ₗ.[R] G} {f : E →ₗ.[R] F} (x : (g ∘ᵣ f).domain) : f ⟨x, x.2.2⟩ ∈ g.domain := - (mem_compRestricted_domain_iff.mp x.2).choose_spec - -@[simp] -lemma compRestricted_apply {g : F →ₗ.[R] G} {f : E →ₗ.[R] F} (x : (g ∘ᵣ f).domain) : - (g ∘ᵣ f) x = g ⟨f ⟨x, x.2.2⟩, mem_domain_of_mem_compRestricted_domain x⟩ := - rfl - -/-- The zero map is right-absorbing. -/ -@[simp] -lemma compRestricted_zero (g : F →ₗ.[R] G) : g ∘ᵣ (0 : E →ₗ.[R] F) = 0 := by - ext - · simp [mem_compRestricted_domain_iff] - · exact g.map_zero - -lemma compRestricted_assoc {H : Type*} [AddCommGroup H] [Module R H] - (f₁ : G →ₗ.[R] H) (f₂ : F →ₗ.[R] G) (f₃ : E →ₗ.[R] F) : - (f₁ ∘ᵣ f₂) ∘ᵣ f₃ = f₁ ∘ᵣ f₂ ∘ᵣ f₃ := by - ext - · simp only [mem_compRestricted_domain_iff] - tauto - · rfl - -/-- `compRestricted` is the same as `comp` when the range of `f` is contained in `g.domain`. -/ -lemma compRestricted_eq_comp - {g : F →ₗ.[R] G} {f : E →ₗ.[R] F} (h : ∀ x : f.domain, f x ∈ g.domain) : - g ∘ᵣ f = g.comp f h := by - ext x - · change _ ↔ x ∈ f.domain - simp [mem_compRestricted_domain_iff, h] - · rfl - -/-- `compRestricted` is maximal amongst compositions of `g` with domain restrictions of `f`. -/ -lemma comp_le_compRestricted {g : F →ₗ.[R] G} {f : E →ₗ.[R] F} {S : Submodule R E} - (h : ∀ x : (f.domRestrict S).domain, f ⟨x, x.2.2⟩ ∈ g.domain) : - g.comp (f.domRestrict S) h ≤ g ∘ᵣ f := - ⟨fun x hx ↦ mem_compRestricted_domain_iff.mpr ⟨hx.2, h ⟨x, hx⟩⟩, by aesop⟩ - -lemma compRestricted_mono_left {g g' : F →ₗ.[R] G} (h : g ≤ g') (f : E →ₗ.[R] F) : - g ∘ᵣ f ≤ g' ∘ᵣ f := by - constructor - · intro x hx - obtain ⟨hx', hfx⟩ := mem_compRestricted_domain_iff.mp hx - exact mem_compRestricted_domain_iff.mpr ⟨hx', h.1 hfx⟩ - · intro x y hxy - exact @h.2 ⟨f ⟨x, x.2.2⟩, mem_domain_of_mem_compRestricted_domain x⟩ - ⟨f ⟨y, y.2.2⟩, mem_domain_of_mem_compRestricted_domain y⟩ (by simp [hxy]) - -lemma compRestricted_mono_right (g : F →ₗ.[R] G) {f f' : E →ₗ.[R] F} (h : f ≤ f') : - g ∘ᵣ f ≤ g ∘ᵣ f' := by - constructor - · intro x hx - obtain ⟨hx', hfx⟩ := mem_compRestricted_domain_iff.mp hx - exact mem_compRestricted_domain_iff.mpr ⟨h.1 hx', (@h.2 ⟨x, hx'⟩ ⟨x, h.1 hx'⟩ rfl) ▸ hfx⟩ - · intro x y hxy - simp only [compRestricted_apply, @h.2 ⟨x, x.2.2⟩ ⟨y, y.2.2⟩ hxy] - -@[simp] -lemma neg_compRestricted (g : F →ₗ.[R] G) (f : E →ₗ.[R] F) : (-g) ∘ᵣ f = -g ∘ᵣ f := rfl - -@[simp] -lemma compRestricted_neg (g : F →ₗ.[R] G) (f : E →ₗ.[R] F) : g ∘ᵣ (-f) = -g ∘ᵣ f := by - ext x hx hx' - · simp [mem_compRestricted_domain_iff] - · obtain ⟨h, h'⟩ := mem_compRestricted_domain_iff.mp hx' - exact g.toFun.map_neg ⟨f ⟨x, h⟩, h'⟩ - -lemma add_compRestricted (g₁ g₂ : F →ₗ.[R] G) (f : E →ₗ.[R] F) : - (g₁ + g₂) ∘ᵣ f = g₁ ∘ᵣ f + g₂ ∘ᵣ f := by - ext x hx hx' - · simp only [mem_compRestricted_domain_iff, add_domain, mem_inf] - tauto - · simp [add_apply] - -lemma sub_compRestricted (g₁ g₂ : F →ₗ.[R] G) (f : E →ₗ.[R] F) : - (g₁ - g₂) ∘ᵣ f = g₁ ∘ᵣ f - g₂ ∘ᵣ f := by - simp [sub_eq_add_neg, add_compRestricted] - -lemma compRestricted_add_ge (g : F →ₗ.[R] G) (f₁ f₂ : E →ₗ.[R] F) : - g ∘ᵣ f₁ + g ∘ᵣ f₂ ≤ g ∘ᵣ (f₁ + f₂) := by - constructor - · intro x hx - obtain ⟨h₁, h₁'⟩ := mem_compRestricted_domain_iff.mp hx.1 - obtain ⟨h₂, h₂'⟩ := mem_compRestricted_domain_iff.mp hx.2 - exact mem_compRestricted_domain_iff.mpr ⟨⟨h₁, h₂⟩, add_mem h₁' h₂'⟩ - · intro x y hxy - obtain ⟨h₁, h₁'⟩ := mem_compRestricted_domain_iff.mp x.2.1 - obtain ⟨h₂, h₂'⟩ := mem_compRestricted_domain_iff.mp x.2.2 - simp [← hxy, add_apply, ← g.map_add ⟨f₁ ⟨x, h₁⟩, h₁'⟩ ⟨f₂ ⟨x, h₂⟩, h₂'⟩] - -lemma compRestricted_sub_ge (g : F →ₗ.[R] G) (f₁ f₂ : E →ₗ.[R] F) : - g ∘ᵣ f₁ - g ∘ᵣ f₂ ≤ g ∘ᵣ (f₁ - f₂) := by - simp only [sub_eq_add_neg, ← compRestricted_neg] - exact compRestricted_add_ge g f₁ (-f₂) - -lemma compRestricted_smul {S : Type*} [DivisionRing S] - [Module S E] [Module S F] [Module S G] [SMulCommClass S S F] [SMulCommClass S S G] - {c : S} (hc : c ≠ 0) (g : F →ₗ.[S] G) (f : E →ₗ.[S] F) : - g ∘ᵣ (c • f) = c • (g ∘ᵣ f) := by - ext x hx hx' - · simp [mem_compRestricted_domain_iff, g.domain.smul_mem_iff hc] - · obtain ⟨h, h'⟩ := mem_compRestricted_domain_iff.mp (smul_domain c (g ∘ᵣ f) ▸ hx') - exact g.toFun.map_smul c ⟨f ⟨x, h⟩, h'⟩ - -@[simp] -lemma smul_compRestricted {M : Type*} [Monoid M] [DistribMulAction M G] [SMulCommClass R M G] - (c : M) (g : F →ₗ.[R] G) (f : E →ₗ.[R] F) : - (c • g) ∘ᵣ f = c • (g ∘ᵣ f) := by - ext - · simp [compRestricted_domain] - · simp - -end - -/-! -### A.4. Monoid - -Partial linear maps `E →ₗ.[R] E` with `compRestricted` for multiplication and -the identity map (domain `⊤`) for `1` comprise a monoid. --/ - -instance instMonoid : Monoid (E →ₗ.[R] E) where - mul := compRestricted - mul_assoc := compRestricted_assoc - one := ⟨⊤, topEquiv.toLinearMap⟩ - one_mul f := by - change ⟨⊤, topEquiv.toLinearMap⟩ ∘ᵣ f = f - ext - · simp [mem_compRestricted_domain_iff] - · rfl - mul_one f := by - change f ∘ᵣ ⟨⊤, topEquiv.toLinearMap⟩ = f - ext - · simp [mem_compRestricted_domain_iff] - · rfl - -lemma mul_def (f₁ f₂ : E →ₗ.[R] E) : f₁ * f₂ = f₁ ∘ᵣ f₂ := rfl - -@[simp] -lemma one_domain : (1 : E →ₗ.[R] E).domain = ⊤ := rfl - -@[simp] -lemma one_toFun : (1 : E →ₗ.[R] E).toFun = topEquiv.toLinearMap := rfl - -@[simp] -lemma one_coe : (1 : E →ₗ.[R] E).toFun' = ⇑topEquiv.toLinearMap := rfl - -/-! -### A.5. Inequalities --/ - -section - -variable (f f₁ f₂ f₃ : E →ₗ.[R] F) {g g₁ g₂ : E →ₗ.[R] F} - -lemma sub_le_zero : f - f ≤ 0 := ⟨le_top, by simp [sub_apply]⟩ - -lemma neg_add_le_zero : -f + f ≤ 0 := ⟨le_top, by simp [add_apply]⟩ - -lemma le_iff_neg_le_neg : g₁ ≤ g₂ ↔ -g₁ ≤ -g₂ := - ⟨fun ⟨h, h'⟩ ↦ ⟨h, fun _ _ h'' ↦ by simp [h' h'']⟩, fun ⟨h, _⟩ ↦ ⟨h, fun _ _ _ ↦ by aesop⟩⟩ - -lemma le_neg_iff_neg_le : g₁ ≤ -g₂ ↔ -g₁ ≤ g₂ := by rw [le_iff_neg_le_neg, neg_neg] - -lemma add_sub_le_cancel : f₁ + (f₂ - f₁) ≤ f₂ := - ⟨by simp [add_domain, sub_domain], fun _ _ h ↦ by simp [add_apply, sub_apply, h]⟩ - -lemma add_sub_le_cancel_left : f₁ + f₂ - f₁ ≤ f₂ := add_sub_assoc f₁ f₂ f₁ ▸ add_sub_le_cancel f₁ f₂ - -lemma add_sub_le_cancel_right : f₁ + f₂ - f₂ ≤ f₁ := add_comm f₁ f₂ ▸ add_sub_le_cancel_left f₂ f₁ - -lemma add_add_sub_le_cancel : f₁ + f₂ + (f₃ - f₂) ≤ f₁ + f₃ := - ⟨fun _ _ ↦ by simp_all [add_domain, sub_domain], fun _ _ h ↦ by simp [add_apply, sub_apply, h]⟩ - -lemma add_sub_sub_le_cancel : f₁ + f₂ - (f₁ - f₃) ≤ f₂ + f₃ := - ⟨fun _ _ ↦ by simp_all [add_domain, sub_domain], fun _ _ h ↦ by simp [add_apply, sub_apply, h]⟩ - -lemma sub_sub_sub_le_cancel_right : f₁ - f₂ - (f₃ - f₂) ≤ f₁ - f₃ := by - simp only [sub_eq_add_neg, neg_add] - exact sub_eq_add_neg (-f₃) (-f₂) ▸ add_add_sub_le_cancel f₁ (-f₂) (-f₃) - -lemma sub_sub_sub_le_cancel_left : f₁ - f₂ - (f₁ - f₃) ≤ f₃ - f₂ := - sub_eq_add_neg f₁ f₂ ▸ neg_add_eq_sub f₂ f₃ ▸ add_sub_sub_le_cancel f₁ (-f₂) f₃ - -lemma sub_le_of_le_add (h : g ≤ g₁ + g₂) : g - g₂ ≤ g₁ := by - constructor - · exact (inf_le_of_left_le le_rfl).trans (le_inf_iff.mp <| add_domain g₁ g₂ ▸ h.1).1 - · intro ⟨x, hx⟩ ⟨y, hy⟩ rfl - simp [sub_apply, @h.2 ⟨x, hx.1⟩ ⟨x, ⟨hy, hx.2⟩⟩ rfl, add_apply] - -lemma sub_add_le_cancel : f₁ - f₂ + f₂ ≤ f₁ := - sub_eq_add_neg f₁ f₂ ▸ sub_neg_eq_add _ f₂ ▸ add_sub_le_cancel_right f₁ (-f₂) - -lemma add_le_of_le_sub (h : g ≤ g₁ - g₂) : g + g₂ ≤ g₁ := - sub_neg_eq_add g g₂ ▸ sub_le_of_le_add (sub_eq_add_neg g₁ g₂ ▸ h) - -lemma add_left_le_of_le (h : g₁ ≤ g₂) : f + g₁ ≤ f + g₂ := by - constructor - · simp only [add_domain, le_inf_iff, inf_le_left, true_and] - exact (inf_le_of_right_le le_rfl).trans h.1 - · intro x y hxy - simp_rw [add_apply, @h.2 ⟨x, x.2.2⟩ ⟨y, y.2.2⟩ hxy, hxy] - -lemma add_right_le_of_le (h : g₁ ≤ g₂) : g₁ + f ≤ g₂ + f := - add_comm f g₁ ▸ add_comm f g₂ ▸ add_left_le_of_le f h - -lemma sub_right_le_of_le (h : g₁ ≤ g₂) : g₁ - f ≤ g₂ - f := - sub_eq_add_neg g₁ f ▸ sub_eq_add_neg g₂ f ▸ add_right_le_of_le (-f) h - -lemma sub_left_le_of_le (h : g₁ ≤ g₂) : f - g₁ ≤ f - g₂ := - neg_sub g₁ f ▸ neg_sub g₂ f ▸ le_iff_neg_le_neg.mp (sub_right_le_of_le f h) - -end - -/-! -## A.6. Inverses --/ - -lemma inverse_ker {f : E →ₗ.[R] F} (h_ker : f.toFun.ker = ⊥) : f.inverse.toFun.ker = ⊥ := by - refine LinearMap.ker_eq_bot'.mpr fun ⟨y, hy⟩ hy' ↦ ?_ - obtain ⟨x, hx⟩ := inverse_domain (f := f) ▸ hy - simp_all [inverse_apply_eq (x := x) (y := ⟨y, hy⟩) h_ker hx] - -lemma inverse_inverse {f : E →ₗ.[R] F} (h_ker : f.toFun.ker = ⊥) : f.inverse.inverse = f := by - ext x hx hx' - · rw [inverse_domain, inverse_range h_ker] - · refine inverse_apply_eq (y := ⟨x, hx⟩) (x := ⟨f ⟨x, hx'⟩, by simp [inverse_domain]⟩) ?_ ?_ - · exact inverse_ker h_ker - · exact inverse_apply_eq (y := ⟨f ⟨x, hx'⟩, by simp [inverse_domain]⟩) (x := ⟨x, hx'⟩) h_ker rfl - -lemma inverse_compRestricted_eq {f : E →ₗ.[R] F} (h_ker : f.toFun.ker = ⊥) : - f.inverse ∘ᵣ f = domRestrict 1 f.domain := by - ext x hx hx' - · simp [mem_compRestricted_domain_iff, inverse_domain, ← toFun_eq_coe] - · exact inverse_apply_eq (x := ⟨x, hx.2⟩) h_ker rfl - -lemma compRestricted_inverse_eq {f : E →ₗ.[R] F} (h_ker : f.toFun.ker = ⊥) : - f ∘ᵣ f.inverse = domRestrict 1 f.inverse.domain := by - nth_rw 1 [← inverse_inverse h_ker] - exact inverse_compRestricted_eq (inverse_ker h_ker) - -end General - -/-! -## B. Operators on inner product/Hilbert spaces --/ - -section InnerProductSpaces - open Submodule open InnerProductSpace open InnerProductSpaceSubmodule @@ -451,10 +97,8 @@ variable {U U₁ U₂ : H →ₗ.[ℂ] H'} {W : α → H →ₗ.[ℂ] H'} {V V₁ V₂ : H' →ₗ.[ℂ] H''} -instance : IsScalarTower ℝ ℂ H := IsScalarTower.complexToReal - /-! -### B.1. Definitions +## A. Definitions See `LinearPMap.instStar` and `LinearPMap.isSelfAdjoint_def` for the definition of `IsSelfAdjoint` for `LinearPMap`s. @@ -482,11 +126,11 @@ lemma isEssentiallySelfAdjoint_def [CompleteSpace H] : T.IsEssentiallySelfAdjoint ↔ IsSelfAdjoint T.closure := Iff.rfl /-! -### B.2. Basic properties +## B. Basic properties -/ /-! -#### B.2.1. Dense domain +### B.1. Dense domain -/ lemma HasDenseDomain.isUnbounded_iff_isClosable (h : U.HasDenseDomain) : @@ -542,7 +186,7 @@ lemma pow_hasDenseDomain_of_le h.mono <| pow_sub_mul_pow T hle ▸ compRestricted_domain_le _ _ /-! -#### B.2.2. Closability +### B.2. Closability -/ lemma IsClosable.isClosed_iff (h : U.IsClosable) : U.IsClosed ↔ U.closure = U := by @@ -623,7 +267,7 @@ lemma closure_smul (U : H →ₗ.[ℂ] H') {c : ℂ} (hc : c ≠ 0) : (c • U). · rw [closure_def' h, closure_def' <| (not_congr <| IsClosable.smul_iff hc).mpr h] /-! -#### B.2.3. Adjoints +### B.3. Adjoints -/ @[simp] @@ -720,7 +364,7 @@ lemma adjoint_pow_le_pow_adjoint [CompleteSpace H] {n : ℕ} (h : (T ^ n).HasDen exact pow_succ' T† n ▸ compRestricted_mono_right T† (ih hTn) /-! -#### B.2.4. Continuity / boundedness +### B.4. Continuity / boundedness -/ /-- `f : E →ₗ[𝕜] F` is continuous iff there exists `M > 0` s.t. `‖f x‖ ≤ M * ‖x‖` for all `x : E`. @@ -877,11 +521,11 @@ lemma IsClosed.sub_continuous [CompleteSpace H'] sub_eq_add_neg U₁ U₂ ▸ h₁.add_continuous h₂.neg h /-! -### B.3. Classes of operators +## C. Classes of operators -/ /-! -#### B.3.1. Symmetric operators +### C.1. Symmetric operators -/ /-- The analogue of `inner_map_polarization` for LinearPMap. -/ @@ -995,7 +639,7 @@ lemma IsSymmetric.of_le (h₁ : T₁.IsSymmetric) (h_le : T₂ ≤ T₁) : T₂. exact hx ▸ hy ▸ h₁ ⟨x, h_le.1 x.2⟩ ⟨y, h_le.1 y.2⟩ /-! -#### B.3.2. Self-adjoint operators +### C.2. Self-adjoint operators -/ lemma IsSelfAdjoint.isSymmetric [CompleteSpace H] (h : IsSelfAdjoint T) : T.IsSymmetric := by @@ -1038,7 +682,7 @@ lemma IsSelfAdjoint.neg [CompleteSpace H] (h : IsSelfAdjoint T) : IsSelfAdjoint neg_eq_neg_one_smul T ▸ smul h (by norm_num) (by norm_num) /-! -#### B.3.3. Essentially self-adjoint operators +### C.3. Essentially self-adjoint operators -/ lemma IsEssentiallySelfAdjoint.hasDenseDomain [CompleteSpace H] (h : T.IsEssentiallySelfAdjoint) : @@ -1085,7 +729,7 @@ lemma IsEssentiallySelfAdjoint.neg [CompleteSpace H] (h : T.IsEssentiallySelfAdj neg_eq_neg_one_smul T ▸ h.smul (by norm_num) (by norm_num) /-! -#### B.3.4. Unbounded operators +### C.4. Unbounded operators -/ lemma IsUnbounded.hasDenseDomain (h : U.IsUnbounded) : U.HasDenseDomain := h.1 @@ -1156,6 +800,4 @@ lemma isUnbounded_of_dense_of_isSymmetric' [CompleteSpace H] (mk E (E.subtype ∘ₗ f)).IsUnbounded := ⟨hE, IsSymmetric.isClosable h hE⟩ -end InnerProductSpaces - end LinearPMap diff --git a/docs/references.bib b/docs/references.bib index 0b6e3b95c..f5063b818 100644 --- a/docs/references.bib +++ b/docs/references.bib @@ -100,6 +100,17 @@ @Article{ raynor2021graphical publisher = {Elsevier} } +@Book{ Reed1972, + author = {Reed, Michael and Simon, Barry}, + title = {Functional Analysis}, + series = {Methods of Modern Mathematical Physics}, + volume = {1}, + year = {1972}, + publisher = {Academic Press}, + isbn = {978-0-12-585001-8}, + doi = {10.1016/B978-0-12-585001-8.X5001-6} +} + @Book{ Schmudgen2012, author = {Konrad Schm{\"u}dgen}, title = {Unbounded Self-Adjoint Operators on Hilbert Space},