From 81dfb72955e73a0ca0fd20c946b99056a11d8a81 Mon Sep 17 00:00:00 2001 From: gloges Date: Fri, 20 Mar 2026 09:54:04 +0900 Subject: [PATCH 1/5] feat: zero --- .../DDimensions/Operators/Unbounded.lean | 39 ++++++++++++++++++- 1 file changed, 37 insertions(+), 2 deletions(-) diff --git a/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean b/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean index 9410fc6ea..7085566e2 100644 --- a/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean +++ b/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean @@ -33,6 +33,9 @@ Definitions: - A. Definition - B. Basic identities +- C. Instances + - C.1. Partial order + - C.2. Zero - C. Partial order - D. Closure - E. Adjoint @@ -112,18 +115,50 @@ lemma inner_map_polarization' {T : UnboundedOperator H H} (x y : T.domain) : end /-! -## C. Partial order +## C. Instances +-/ + +section + +open Classical + +/-! +### C.1. Partial order Unbounded operators inherit the structure of a poset from `LinearPMap`, but *not* that of a `SemilatticeInf` because `U₁.domain ⊓ U₂.domain` may not be dense. -/ -instance partialOrder : PartialOrder (UnboundedOperator H H') where +instance : PartialOrder (UnboundedOperator H H') where le U₁ U₂ := U₁.toLinearPMap ≤ U₂.toLinearPMap le_refl _ := le_refl _ le_trans _ _ _ h₁₂ h₂₃ := le_trans h₁₂ h₂₃ le_antisymm _ _ h h' := ext <| le_antisymm h h' +/-! +### C.2. Zero +-/ + +-- A zero LinearPMap (any domain) is closable +lemma isClosable_of_zero {E F : Type*} [NormedAddCommGroup E] [InnerProductSpace ℂ E] + [NormedAddCommGroup F] [InnerProductSpace ℂ F] {f : LinearPMap ℂ E F} (hf : f.toFun' = 0) : + f.IsClosable := by + use f.graph.topologicalClosure.toLinearPMap + refine Eq.symm <| toLinearPMap_graph_eq f.graph.topologicalClosure fun x hx _ ↦ ?_ + obtain ⟨b, hb, hb'⟩ := mem_closure_iff_seq_limit.mp hx + have (n : ℕ) : (b n).2 = 0 := by specialize hb n; simp_all + rw [nhds_prod_eq, Filter.tendsto_prod_iff'] at hb' + simp_all + +instance : Zero (UnboundedOperator H H') := ⟨0, by simp, isClosable_of_zero rfl⟩ + +@[simp] +lemma zero_toLinearPMap : (0 : UnboundedOperator H H').toLinearPMap = 0 := rfl + +instance : Inhabited (UnboundedOperator H H') := ⟨instZero.zero⟩ + +end + /-! ## D. Closure -/ From b6b5b5e6c2783ed8f93c7237655a53386a1ff689 Mon Sep 17 00:00:00 2001 From: gloges Date: Fri, 20 Mar 2026 09:56:38 +0900 Subject: [PATCH 2/5] feat: addition --- .../DDimensions/Operators/Unbounded.lean | 75 ++++++++++++++++++- 1 file changed, 74 insertions(+), 1 deletion(-) diff --git a/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean b/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean index 7085566e2..0692cba88 100644 --- a/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean +++ b/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean @@ -36,7 +36,7 @@ Definitions: - C. Instances - C.1. Partial order - C.2. Zero -- C. Partial order + - C.3. AddZeroClass - D. Closure - E. Adjoint - F. Symmetric operators @@ -157,6 +157,79 @@ lemma zero_toLinearPMap : (0 : UnboundedOperator H H').toLinearPMap = 0 := rfl instance : Inhabited (UnboundedOperator H H') := ⟨instZero.zero⟩ +/-! +### C.3. AddZeroClass + +In defining addition for unbounded operators we use two junk values. +- If `U₁.domain ∩ U₂.domain` is not dense, then `U₁ + U₂ = 0` (domain `⊤`) +- If `U₁.domain ∩ U₂.domain` is dense but `U₁.toLinearPMap + U₂.toLinearPMap` is not closable, + then `U₁ + U₂ = 0` with domain `U₁.domain ∩ U₂.domain`. +This ensures that distributivity, `c • (U₁ + U₂) = c • U₁ + c • U₂`, holds for `(c : ℂ) = 0`. +-/ + +noncomputable instance : Add (UnboundedOperator H H') where + add U₁ U₂ := + if hD : Dense (U₁.domain ⊓ U₂.domain : Set H) then + if hC : (U₁.toLinearPMap + U₂.toLinearPMap).IsClosable then + ⟨U₁.toLinearPMap + U₂.toLinearPMap, hD, hC⟩ + else ⟨⟨U₁.domain ⊓ U₂.domain, 0⟩, hD, isClosable_of_zero rfl⟩ + else 0 + +lemma add_domain_of_dense {U₁ U₂ : UnboundedOperator H H'} + (hD : Dense (U₁.domain ⊓ U₂.domain : Set H)) : (U₁ + U₂).domain = U₁.domain ⊓ U₂.domain := by + rw [HAdd.hAdd, instHAdd, Add.add, instAdd] + by_cases hC : (U₁.toLinearPMap + U₂.toLinearPMap).IsClosable + · simp only [hD, hC, ↓reduceDIte, LinearPMap.add_domain] + · simp only [hD, hC, ↓reduceDIte] + +lemma add_domain_of_not_dense {U₁ U₂ : UnboundedOperator H H'} + (hD : ¬Dense (U₁.domain ⊓ U₂.domain : Set H)) : (U₁ + U₂).domain = ⊤ := by + rw [HAdd.hAdd, instHAdd, Add.add, instAdd] + simp only [hD, ↓reduceDIte, zero_toLinearPMap, zero_domain] + +lemma mem_domain_of_dense {U₁ U₂ : UnboundedOperator H H'} + (hD : Dense (U₁.domain ⊓ U₂.domain : Set H)) (ψ : (U₁ + U₂).domain) : + ↑ψ ∈ U₁.domain ∧ ↑ψ ∈ U₂.domain := + mem_inf.mp <| (add_domain_of_dense hD) ▸ ψ.2 + +lemma add_toLinearPMap_of_dense_closable {U₁ U₂ : UnboundedOperator H H'} + (hD : Dense (U₁.domain ⊓ U₂.domain : Set H)) + (hC : (U₁.toLinearPMap + U₂.toLinearPMap).IsClosable) : + (U₁ + U₂).toLinearPMap = U₁.toLinearPMap + U₂.toLinearPMap := by + rw [HAdd.hAdd, instHAdd, Add.add, instAdd] + simp only [hD, hC, ↓reduceDIte] + +lemma add_toLinearPMap_of_dense_not_closable {U₁ U₂ : UnboundedOperator H H'} + (hD : Dense (U₁.domain ⊓ U₂.domain : Set H)) + (hC : ¬(U₁.toLinearPMap + U₂.toLinearPMap).IsClosable) : + (U₁ + U₂).toLinearPMap = ⟨U₁.domain ⊓ U₂.domain, 0⟩ := by + rw [HAdd.hAdd, instHAdd, Add.add, instAdd] + simp only [hD, hC, ↓reduceDIte] + +lemma add_toLinearPMap_of_not_dense {U₁ U₂ : UnboundedOperator H H'} + (hD : ¬Dense (U₁.domain ⊓ U₂.domain : Set H)) : (U₁ + U₂).toLinearPMap = 0 := by + rw [HAdd.hAdd, instHAdd, Add.add, instAdd] + simp only [hD, ↓reduceDIte, zero_toLinearPMap] + +lemma add_apply_of_dense_closable {U₁ U₂ : UnboundedOperator H H'} + (hD : Dense (U₁.domain ⊓ U₂.domain : Set H)) + (hC : (U₁.toLinearPMap + U₂.toLinearPMap).IsClosable) (ψ : (U₁ + U₂).domain) : + (U₁ + U₂) ψ = U₁ ⟨ψ, (mem_domain_of_dense hD ψ).1⟩ + U₂ ⟨ψ, (mem_domain_of_dense hD ψ).2⟩ := by + obtain ⟨_, hb⟩ := LinearPMap.dExt_iff.mp <| add_toLinearPMap_of_dense_closable hD hC + simp only [Subtype.forall] at hb + specialize hb ψ ψ.2 ψ (mem_domain_of_dense hD ψ) rfl + simp_all [LinearPMap.add_apply] + +noncomputable instance : AddZeroClass (UnboundedOperator H H') where + zero_add U := by + apply UnboundedOperator.ext + rw [← zero_add U.toLinearPMap] + exact add_toLinearPMap_of_dense_closable (by simp [U.dense_domain]) (by simp [U.is_closable]) + add_zero U := by + apply UnboundedOperator.ext + rw [← add_zero U.toLinearPMap] + exact add_toLinearPMap_of_dense_closable (by simp [U.dense_domain]) (by simp [U.is_closable]) + end /-! From e7e1d1378936248f3939d3474ae31c7bc054c94d Mon Sep 17 00:00:00 2001 From: gloges Date: Fri, 20 Mar 2026 10:14:31 +0900 Subject: [PATCH 3/5] feat: assoc --- .../DDimensions/Operators/Unbounded.lean | 27 +++++++++++++++++++ 1 file changed, 27 insertions(+) diff --git a/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean b/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean index 0692cba88..e83f3f834 100644 --- a/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean +++ b/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean @@ -230,6 +230,33 @@ noncomputable instance : AddZeroClass (UnboundedOperator H H') where rw [← add_zero U.toLinearPMap] exact add_toLinearPMap_of_dense_closable (by simp [U.dense_domain]) (by simp [U.is_closable]) +lemma add_assoc {U₁ U₂ U₃ : UnboundedOperator H H'} + (hD : Dense (U₁.domain ⊓ U₂.domain ⊓ U₃.domain : Set H)) (hC₁₂ : (U₁.1 + U₂.1).IsClosable) + (hC₂₃ : (U₂.1 + U₃.1).IsClosable) : U₁ + U₂ + U₃ = U₁ + (U₂ + U₃) := by + have hD' : Dense (U₁.domain ⊓ (U₂.domain ⊓ U₃.domain) : Set H) := by simp_all [Set.inter_assoc] + have hD₁₂ : Dense (U₁.domain ⊓ U₂.domain : Set H) := Dense.mono Set.inter_subset_left hD + have hD₂₃ : Dense (U₂.domain ⊓ U₃.domain : Set H) := Dense.mono Set.inter_subset_right hD' + have hD₁₂' : (U₁ + U₂).domain = U₁.domain ⊓ U₂.domain := add_domain_of_dense hD₁₂ + have hD₂₃' : (U₂ + U₃).domain = U₂.domain ⊓ U₃.domain := add_domain_of_dense hD₂₃ + have hD₁₂'' : Dense ((U₁ + U₂).domain ⊓ U₃.domain : Set H) := hD₁₂' ▸ hD + have hD₂₃'' : Dense (U₁.domain ⊓ (U₂ + U₃).domain : Set H) := hD₂₃' ▸ hD' + have h₁₂ : (U₁ + U₂).1 = U₁.1 + U₂.1 := add_toLinearPMap_of_dense_closable hD₁₂ hC₁₂ + have h₂₃ : (U₂ + U₃).1 = U₂.1 + U₃.1 := add_toLinearPMap_of_dense_closable hD₂₃ hC₂₃ + apply UnboundedOperator.ext + by_cases hC : (U₁.1 + U₂.1 + U₃.1).IsClosable + · have hC' : (U₁.1 + (U₂.1 + U₃.1)).IsClosable := by grind + have h12 := add_toLinearPMap_of_dense_closable hD₁₂ hC₁₂ ▸ hC + have h23 := add_toLinearPMap_of_dense_closable hD₂₃ hC₂₃ ▸ hC' + rw [add_toLinearPMap_of_dense_closable hD₁₂'' h12] + rw [add_toLinearPMap_of_dense_closable hD₂₃'' h23] + grind + · have hC' : ¬(U₁.1 + (U₂.1 + U₃.1)).IsClosable := by grind + rw [add_toLinearPMap_of_dense_not_closable hD₁₂'' (h₁₂ ▸ hC)] + rw [add_toLinearPMap_of_dense_not_closable hD₂₃'' (h₂₃ ▸ hC')] + ext + · simp [hD₁₂', hD₂₃', and_assoc] + · simp + end /-! From ba5150a4503fd2c7098c901da5af0cb895e0e9bd Mon Sep 17 00:00:00 2001 From: gloges Date: Sat, 21 Mar 2026 13:00:09 +0900 Subject: [PATCH 4/5] generalized add_assoc --- .../DDimensions/Operators/Unbounded.lean | 50 ++++++++++--------- 1 file changed, 26 insertions(+), 24 deletions(-) diff --git a/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean b/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean index e83f3f834..27e398859 100644 --- a/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean +++ b/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean @@ -231,31 +231,33 @@ noncomputable instance : AddZeroClass (UnboundedOperator H H') where exact add_toLinearPMap_of_dense_closable (by simp [U.dense_domain]) (by simp [U.is_closable]) lemma add_assoc {U₁ U₂ U₃ : UnboundedOperator H H'} - (hD : Dense (U₁.domain ⊓ U₂.domain ⊓ U₃.domain : Set H)) (hC₁₂ : (U₁.1 + U₂.1).IsClosable) - (hC₂₃ : (U₂.1 + U₃.1).IsClosable) : U₁ + U₂ + U₃ = U₁ + (U₂ + U₃) := by - have hD' : Dense (U₁.domain ⊓ (U₂.domain ⊓ U₃.domain) : Set H) := by simp_all [Set.inter_assoc] - have hD₁₂ : Dense (U₁.domain ⊓ U₂.domain : Set H) := Dense.mono Set.inter_subset_left hD - have hD₂₃ : Dense (U₂.domain ⊓ U₃.domain : Set H) := Dense.mono Set.inter_subset_right hD' - have hD₁₂' : (U₁ + U₂).domain = U₁.domain ⊓ U₂.domain := add_domain_of_dense hD₁₂ - have hD₂₃' : (U₂ + U₃).domain = U₂.domain ⊓ U₃.domain := add_domain_of_dense hD₂₃ - have hD₁₂'' : Dense ((U₁ + U₂).domain ⊓ U₃.domain : Set H) := hD₁₂' ▸ hD - have hD₂₃'' : Dense (U₁.domain ⊓ (U₂ + U₃).domain : Set H) := hD₂₃' ▸ hD' - have h₁₂ : (U₁ + U₂).1 = U₁.1 + U₂.1 := add_toLinearPMap_of_dense_closable hD₁₂ hC₁₂ - have h₂₃ : (U₂ + U₃).1 = U₂.1 + U₃.1 := add_toLinearPMap_of_dense_closable hD₂₃ hC₂₃ + (hD₁₂ : Dense (U₁.domain ⊓ U₂.domain : Set H)) (hC₁₂ : (U₁.1 + U₂.1).IsClosable) + (hD₂₃ : Dense (U₂.domain ⊓ U₃.domain : Set H)) (hC₂₃ : (U₂.1 + U₃.1).IsClosable) : + U₁ + U₂ + U₃ = U₁ + (U₂ + U₃) := by apply UnboundedOperator.ext - by_cases hC : (U₁.1 + U₂.1 + U₃.1).IsClosable - · have hC' : (U₁.1 + (U₂.1 + U₃.1)).IsClosable := by grind - have h12 := add_toLinearPMap_of_dense_closable hD₁₂ hC₁₂ ▸ hC - have h23 := add_toLinearPMap_of_dense_closable hD₂₃ hC₂₃ ▸ hC' - rw [add_toLinearPMap_of_dense_closable hD₁₂'' h12] - rw [add_toLinearPMap_of_dense_closable hD₂₃'' h23] - grind - · have hC' : ¬(U₁.1 + (U₂.1 + U₃.1)).IsClosable := by grind - rw [add_toLinearPMap_of_dense_not_closable hD₁₂'' (h₁₂ ▸ hC)] - rw [add_toLinearPMap_of_dense_not_closable hD₂₃'' (h₂₃ ▸ hC')] - ext - · simp [hD₁₂', hD₂₃', and_assoc] - · simp + by_cases hD : Dense (U₁.domain ⊓ U₂.domain ⊓ U₃.domain : Set H) + · have hD' : Dense (U₁.domain ⊓ (U₂.domain ⊓ U₃.domain) : Set H) := by grind + have hD₁₂' : (U₁ + U₂).domain = U₁.domain ⊓ U₂.domain := add_domain_of_dense hD₁₂ + have hD₂₃' : (U₂ + U₃).domain = U₂.domain ⊓ U₃.domain := add_domain_of_dense hD₂₃ + have h₁₂ : (U₁ + U₂).1 = U₁.1 + U₂.1 := add_toLinearPMap_of_dense_closable hD₁₂ hC₁₂ + have h₂₃ : (U₂ + U₃).1 = U₂.1 + U₃.1 := add_toLinearPMap_of_dense_closable hD₂₃ hC₂₃ + by_cases hC : (U₁.1 + U₂.1 + U₃.1).IsClosable + · -- No junk values anywhere: addition is associative + have hC' : (U₁.1 + (U₂.1 + U₃.1)).IsClosable := by grind + rw [add_toLinearPMap_of_dense_closable (by simp_all) (h₁₂ ▸ hC), h₁₂, + add_toLinearPMap_of_dense_closable (by simp_all) (h₂₃ ▸ hC'), h₂₃] + grind + · -- D(U₁) ∩ D(U₂) ∩ D(U₃) is dense but neither side is closable: + -- both sides are the junk zero operator with domain D(U₁) ∩ D(U₂) ∩ D(U₃) + have hC' : ¬(U₁.1 + (U₂.1 + U₃.1)).IsClosable := by grind + rw [add_toLinearPMap_of_dense_not_closable (by simp_all) (h₁₂ ▸ hC), hD₁₂', + add_toLinearPMap_of_dense_not_closable (by simp_all) (h₂₃ ▸ hC'), hD₂₃'] + grind + · -- D(U₁) ∩ D(U₂) ∩ D(U₃) is not dense: both sides are the junk zero operator with domain ⊤ + have hD' : ¬Dense (U₁.domain ⊓ (U₂.domain ⊓ U₃.domain) : Set H) := by grind + have hD₁₂' : ¬Dense ((U₁ + U₂).domain ⊓ U₃.domain : Set H) := add_domain_of_dense hD₁₂ ▸ hD + have hD₂₃' : ¬Dense (U₁.domain ⊓ (U₂ + U₃).domain : Set H) := add_domain_of_dense hD₂₃ ▸ hD' + rw [add_toLinearPMap_of_not_dense hD₁₂', add_toLinearPMap_of_not_dense hD₂₃'] end From 4ddc28a760219b59d1786c82bb7c1cdaeea9dd60 Mon Sep 17 00:00:00 2001 From: gloges Date: Sat, 21 Mar 2026 13:00:24 +0900 Subject: [PATCH 5/5] doc strings --- .../DDimensions/Operators/Unbounded.lean | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean b/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean index 27e398859..d5616e926 100644 --- a/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean +++ b/PhysLean/QuantumMechanics/DDimensions/Operators/Unbounded.lean @@ -175,6 +175,7 @@ noncomputable instance : Add (UnboundedOperator H H') where else ⟨⟨U₁.domain ⊓ U₂.domain, 0⟩, hD, isClosable_of_zero rfl⟩ else 0 +/-- The domain of `U₁ + U₂` is `D(U₁) ∩ D(U₂)` when it is dense. -/ lemma add_domain_of_dense {U₁ U₂ : UnboundedOperator H H'} (hD : Dense (U₁.domain ⊓ U₂.domain : Set H)) : (U₁ + U₂).domain = U₁.domain ⊓ U₂.domain := by rw [HAdd.hAdd, instHAdd, Add.add, instAdd] @@ -182,6 +183,7 @@ lemma add_domain_of_dense {U₁ U₂ : UnboundedOperator H H'} · simp only [hD, hC, ↓reduceDIte, LinearPMap.add_domain] · simp only [hD, hC, ↓reduceDIte] +/-- The junk value for `U₁ + U₂` has domain all of `H` when `D(U₁) ∩ D(U₂)` is not dense. -/ lemma add_domain_of_not_dense {U₁ U₂ : UnboundedOperator H H'} (hD : ¬Dense (U₁.domain ⊓ U₂.domain : Set H)) : (U₁ + U₂).domain = ⊤ := by rw [HAdd.hAdd, instHAdd, Add.add, instAdd] @@ -192,6 +194,8 @@ lemma mem_domain_of_dense {U₁ U₂ : UnboundedOperator H H'} ↑ψ ∈ U₁.domain ∧ ↑ψ ∈ U₂.domain := mem_inf.mp <| (add_domain_of_dense hD) ▸ ψ.2 +/-- `U₁ + U₂` is the unbounded operator corresponding to `U₁.toLinearPMap + U₂.toLinearPMap`, + provided it is both densely defined and closable. -/ lemma add_toLinearPMap_of_dense_closable {U₁ U₂ : UnboundedOperator H H'} (hD : Dense (U₁.domain ⊓ U₂.domain : Set H)) (hC : (U₁.toLinearPMap + U₂.toLinearPMap).IsClosable) : @@ -199,6 +203,7 @@ lemma add_toLinearPMap_of_dense_closable {U₁ U₂ : UnboundedOperator H H'} rw [HAdd.hAdd, instHAdd, Add.add, instAdd] simp only [hD, hC, ↓reduceDIte] +/-- The junk value for `U₁ + U₂` when `D(U₁) ∩ D(U₂)` is dense and `U₁ + U₂` is not closable. -/ lemma add_toLinearPMap_of_dense_not_closable {U₁ U₂ : UnboundedOperator H H'} (hD : Dense (U₁.domain ⊓ U₂.domain : Set H)) (hC : ¬(U₁.toLinearPMap + U₂.toLinearPMap).IsClosable) : @@ -206,11 +211,13 @@ lemma add_toLinearPMap_of_dense_not_closable {U₁ U₂ : UnboundedOperator H H' rw [HAdd.hAdd, instHAdd, Add.add, instAdd] simp only [hD, hC, ↓reduceDIte] +/-- The junk value for `U₁ + U₂` when `D(U₁) ∩ D(U₂)` is not dense. -/ lemma add_toLinearPMap_of_not_dense {U₁ U₂ : UnboundedOperator H H'} (hD : ¬Dense (U₁.domain ⊓ U₂.domain : Set H)) : (U₁ + U₂).toLinearPMap = 0 := by rw [HAdd.hAdd, instHAdd, Add.add, instAdd] simp only [hD, ↓reduceDIte, zero_toLinearPMap] +/-- `(U₁ + U₂)ψ = U₁ψ + U₂ψ` provided `U₁ + U₂` is not given by a junk value. -/ lemma add_apply_of_dense_closable {U₁ U₂ : UnboundedOperator H H'} (hD : Dense (U₁.domain ⊓ U₂.domain : Set H)) (hC : (U₁.toLinearPMap + U₂.toLinearPMap).IsClosable) (ψ : (U₁ + U₂).domain) : @@ -230,6 +237,8 @@ noncomputable instance : AddZeroClass (UnboundedOperator H H') where rw [← add_zero U.toLinearPMap] exact add_toLinearPMap_of_dense_closable (by simp [U.dense_domain]) (by simp [U.is_closable]) +/-- Addition of unbounded operators is associative when neither of the intermediate additions, + `U₁ + U₂` and `U₂ + U₃`, is given by a junk value. -/ lemma add_assoc {U₁ U₂ U₃ : UnboundedOperator H H'} (hD₁₂ : Dense (U₁.domain ⊓ U₂.domain : Set H)) (hC₁₂ : (U₁.1 + U₂.1).IsClosable) (hD₂₃ : Dense (U₂.domain ⊓ U₃.domain : Set H)) (hC₂₃ : (U₂.1 + U₃.1).IsClosable) :