From 56d26eedeef1933a1db56dfab5304a9d23dd5c69 Mon Sep 17 00:00:00 2001
From: gloges <gerg1995@gmail.com>
Date: Mon, 20 Jul 2026 12:00:13 +0900
Subject: [PATCH 1/6] memHS lemma

---
 Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Basic.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Basic.lean b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Basic.lean
index edc2bff68..b0f807143 100644
--- a/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Basic.lean
+++ b/Physlib/QuantumMechanics/HilbertSpaces/SpaceD/Basic.lean
@@ -129,6 +129,9 @@ lemma MemHS.sub (hf : MemHS f μ) (hg : MemHS g μ) : MemHS (f - g) μ := MemLp.
 
 lemma MemHS.const_smul (c : ℂ) (hf : MemHS f μ) : MemHS (c • f) μ := MemLp.const_smul hf c
 
+lemma MemHS.const_smul_iff {c : ℂ} (hc : c ≠ 0) : MemHS (c • f) μ ↔ MemHS f μ :=
+  ⟨fun h ↦ inv_smul_smul₀ hc f ▸ h.const_smul c⁻¹, const_smul c⟩
+
 lemma MemHS.ae_eq (hfg : f =ᵐ[μ] g) (hf : MemHS f μ) : MemHS g μ := MemLp.ae_eq hfg hf
 
 lemma MemHS.mono_measure (h : μ' ≤ μ) (hf : MemHS f μ) : MemHS f μ' := MemLp.mono_measure h hf

From 10b95161c94a311d365971f4e190b038e388d393 Mon Sep 17 00:00:00 2001
From: gloges <gerg1995@gmail.com>
Date: Mon, 20 Jul 2026 12:01:04 +0900
Subject: [PATCH 2/6] sections

---
 .../Operators/Multiplication.lean             | 20 +++++++++++++++++--
 1 file changed, 18 insertions(+), 2 deletions(-)

diff --git a/Physlib/QuantumMechanics/Operators/Multiplication.lean b/Physlib/QuantumMechanics/Operators/Multiplication.lean
index b922dad2f..ec94c4fcd 100644
--- a/Physlib/QuantumMechanics/Operators/Multiplication.lean
+++ b/Physlib/QuantumMechanics/Operators/Multiplication.lean
@@ -34,7 +34,11 @@ In this module we introduce unbounded operators defined by multiplication by a f
 - C. Adjoint
   - C.1. Self-adjoint
 - D. Closable & unbounded
-- E. Composition
+- E. Structural properties
+  - E.1. Smul
+  - E.2. Add & sub
+  - E.3. Composition
+- F. Spectrum
 
 ## iv. References
 
@@ -326,7 +330,19 @@ lemma mulOperator_isUnbounded {μ : Measure (Space d)} [IsFiniteMeasureOnCompact
   ⟨mulOperator_hasDenseDomain hf, mulOperator_isClosable hf⟩
 
 /-!
-## E. Composition
+## E. Structural properties
+-/
+
+/-!
+### E.1. Smul & neg
+-/
+
+/-!
+### E.2. Add & sub
+-/
+
+/-!
+### E.3. Composition
 -/
 
 lemma mulOperator_compRestricted_le (μ : Measure (Space d)) (f g : Space d → ℂ) :

From 6f405346f2f5afd4f7ca7b184de17551a5a8b6ff Mon Sep 17 00:00:00 2001
From: gloges <gerg1995@gmail.com>
Date: Mon, 20 Jul 2026 12:01:39 +0900
Subject: [PATCH 3/6] smul & neg

---
 .../Operators/Multiplication.lean             | 25 +++++++++++++++++++
 1 file changed, 25 insertions(+)

diff --git a/Physlib/QuantumMechanics/Operators/Multiplication.lean b/Physlib/QuantumMechanics/Operators/Multiplication.lean
index ec94c4fcd..85ef4fa90 100644
--- a/Physlib/QuantumMechanics/Operators/Multiplication.lean
+++ b/Physlib/QuantumMechanics/Operators/Multiplication.lean
@@ -337,6 +337,31 @@ lemma mulOperator_isUnbounded {μ : Measure (Space d)} [IsFiniteMeasureOnCompact
 ### E.1. Smul & neg
 -/
 
+lemma mulOperator_smul_ge (μ : Measure (Space d)) (c : ℂ) (f : Space d → ℂ) :
+    c • 𝓜 μ f ≤ 𝓜 μ (c • f) := by
+  refine le_of_le_graph fun u h ↦ ?_
+  rw [mem_graph_iff] at *
+  obtain ⟨⟨v, hv⟩, hvu, hvu'⟩ := h
+  have hv' : v ∈ (𝓜 μ (c • f)).domain := by
+    rw [smul_domain, mem_mulOperator_domain_iff] at *
+    simpa using hv.const_smul c
+  refine ⟨⟨v, hv'⟩, hvu, ?_⟩
+  rw [← hvu', ext_iff]
+  filter_upwards [mulOperator_apply_ae ⟨v, hv⟩, mulOperator_apply_ae ⟨v, hv'⟩,
+    coeFn_smul c (𝓜 μ f ⟨v, hv⟩)]
+  simp_all [mul_assoc]
+
+@[simp]
+lemma mulOperator_smul_eq (μ : Measure (Space d)) {c : ℂ} (hc : c ≠ 0) (f : Space d → ℂ) :
+    𝓜 μ (c • f) = c • 𝓜 μ f := by
+  refine (eq_of_le_of_domain_eq (mulOperator_smul_ge μ c f) ?_).symm
+  ext
+  simp [mem_mulOperator_domain_iff, MemHS.const_smul_iff hc]
+
+@[simp]
+lemma mulOperator_neg (μ : Measure (Space d)) (f : Space d → ℂ) : 𝓜 μ (-f) = -𝓜 μ f := by
+  rw [← neg_one_smul ℂ f, mulOperator_smul_eq _ (by norm_num), neg_eq_neg_one_smul]
+
 /-!
 ### E.2. Add & sub
 -/

From 95f7d161e667f2492c0b6884ef8dad39e0c64b2b Mon Sep 17 00:00:00 2001
From: gloges <gerg1995@gmail.com>
Date: Mon, 20 Jul 2026 12:02:33 +0900
Subject: [PATCH 4/6] add & sub

---
 .../Operators/Multiplication.lean             | 21 ++++++++++++++++++-
 1 file changed, 20 insertions(+), 1 deletion(-)

diff --git a/Physlib/QuantumMechanics/Operators/Multiplication.lean b/Physlib/QuantumMechanics/Operators/Multiplication.lean
index 85ef4fa90..0cbe8af53 100644
--- a/Physlib/QuantumMechanics/Operators/Multiplication.lean
+++ b/Physlib/QuantumMechanics/Operators/Multiplication.lean
@@ -104,7 +104,7 @@ lemma mem_mulOperator_domain_iff
   Iff.rfl
 
 lemma mulOperator_apply_ae {μ : Measure (Space d)} {f : Space d → ℂ} (ψ : (𝓜 μ f).domain) :
-    (𝓜 μ f) ψ =ᵐ[μ] f • ψ :=
+    𝓜 μ f ψ =ᵐ[μ] f • ψ :=
   coeFn_mk ψ.prop
 
 /-!
@@ -366,6 +366,25 @@ lemma mulOperator_neg (μ : Measure (Space d)) (f : Space d → ℂ) : 𝓜 μ (
 ### E.2. Add & sub
 -/
 
+lemma mulOperator_add_ge (μ : Measure (Space d)) (f g : Space d → ℂ) :
+    𝓜 μ f + 𝓜 μ g ≤ 𝓜 μ (f + g) := by
+  refine le_of_le_graph fun u h ↦ ?_
+  rw [mem_graph_iff] at *
+  obtain ⟨⟨v, hv⟩, hvu, hvu'⟩ := h
+  have hv' : v ∈ (𝓜 μ (f + g)).domain := by
+    rw [add_domain, Submodule.mem_inf] at hv
+    simpa [add_mul, mem_mulOperator_domain_iff] using hv.1.add hv.2
+  refine ⟨⟨v, hv'⟩, hvu, ?_⟩
+  rw [← hvu', ext_iff]
+  change _ =ᵐ[μ] 𝓜 μ f ⟨v, hv.1⟩ + 𝓜 μ g ⟨v, hv.2⟩
+  filter_upwards [mulOperator_apply_ae ⟨v, hv.1⟩, mulOperator_apply_ae ⟨v, hv.2⟩,
+    mulOperator_apply_ae ⟨v, hv'⟩, coeFn_add (𝓜 μ f ⟨v, hv.1⟩) (𝓜 μ g ⟨v, hv.2⟩)]
+  simp_all [add_mul]
+
+lemma mulOperator_sub_ge (μ : Measure (Space d)) (f g : Space d → ℂ) :
+    𝓜 μ f - 𝓜 μ g ≤ 𝓜 μ (f - g) :=
+  le_of_eq_of_le (by simp [sub_eq_add_neg]) (mulOperator_add_ge μ f (-g))
+
 /-!
 ### E.3. Composition
 -/

From c0955176936b1f51156fefde0eae790a0e520b48 Mon Sep 17 00:00:00 2001
From: gloges <gerg1995@gmail.com>
Date: Tue, 21 Jul 2026 22:12:25 +0900
Subject: [PATCH 5/6] add/sub eq + TODO

---
 .../Operators/Multiplication.lean             | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)

diff --git a/Physlib/QuantumMechanics/Operators/Multiplication.lean b/Physlib/QuantumMechanics/Operators/Multiplication.lean
index 0cbe8af53..b05250b34 100644
--- a/Physlib/QuantumMechanics/Operators/Multiplication.lean
+++ b/Physlib/QuantumMechanics/Operators/Multiplication.lean
@@ -381,10 +381,29 @@ lemma mulOperator_add_ge (μ : Measure (Space d)) (f g : Space d → ℂ) :
     mulOperator_apply_ae ⟨v, hv'⟩, coeFn_add (𝓜 μ f ⟨v, hv.1⟩) (𝓜 μ g ⟨v, hv.2⟩)]
   simp_all [add_mul]
 
+lemma mulOperator_add_eq
+    {μ : Measure (Space d)} (f : Space d → ℂ) {g : Space d → ℂ} (h : (𝓜 μ g).domain = ⊤) :
+    𝓜 μ (f + g) = 𝓜 μ f + 𝓜 μ g := by
+  have hle := mulOperator_add_ge μ f g
+  refine (eq_of_le_of_domain_eq hle ?_).symm
+  refine eq_of_le_of_ge hle.1 fun ψ hψ ↦ ?_
+  have hg : ψ ∈ (𝓜 μ g).domain := by simp [h]
+  simp only [add_domain, Submodule.mem_inf, mem_mulOperator_domain_iff] at *
+  exact ⟨by simpa [add_mul] using hψ.sub hg, hg⟩
+
 lemma mulOperator_sub_ge (μ : Measure (Space d)) (f g : Space d → ℂ) :
     𝓜 μ f - 𝓜 μ g ≤ 𝓜 μ (f - g) :=
   le_of_eq_of_le (by simp [sub_eq_add_neg]) (mulOperator_add_ge μ f (-g))
 
+lemma mulOperator_sub_eq
+    {μ : Measure (Space d)} (f : Space d → ℂ) {g : Space d → ℂ} (h : (𝓜 μ g).domain = ⊤) :
+    𝓜 μ (f - g) = 𝓜 μ f - 𝓜 μ g := by
+  simp [sub_eq_add_neg, mulOperator_add_eq, h]
+
+TODO "`mulOperator_add_eq` has the strong assumption `(𝓜 μ g).domain = ⊤`. Weaken this assumption
+  and/or find other sufficient conditions to ensure the equality `𝓜 μ (f + g) = 𝓜 μ f + 𝓜 μ g`.
+  For example, `f • g ≥ᵐ[μ] 0` or `|f| ≤ᵐ[μ] c • |g|` (with no assumptions on the domains)?"
+
 /-!
 ### E.3. Composition
 -/

From d229d6c93b4453c722d3118095d5eb63891e75b7 Mon Sep 17 00:00:00 2001
From: gloges <gerg1995@gmail.com>
Date: Tue, 21 Jul 2026 22:26:55 +0900
Subject: [PATCH 6/6] simp tags

---
 Physlib/QuantumMechanics/Operators/Multiplication.lean | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/Physlib/QuantumMechanics/Operators/Multiplication.lean b/Physlib/QuantumMechanics/Operators/Multiplication.lean
index b05250b34..75754fd64 100644
--- a/Physlib/QuantumMechanics/Operators/Multiplication.lean
+++ b/Physlib/QuantumMechanics/Operators/Multiplication.lean
@@ -35,7 +35,7 @@ In this module we introduce unbounded operators defined by multiplication by a f
   - C.1. Self-adjoint
 - D. Closable & unbounded
 - E. Structural properties
-  - E.1. Smul
+  - E.1. Smul & neg
   - E.2. Add & sub
   - E.3. Composition
 - F. Spectrum
@@ -381,6 +381,7 @@ lemma mulOperator_add_ge (μ : Measure (Space d)) (f g : Space d → ℂ) :
     mulOperator_apply_ae ⟨v, hv'⟩, coeFn_add (𝓜 μ f ⟨v, hv.1⟩) (𝓜 μ g ⟨v, hv.2⟩)]
   simp_all [add_mul]
 
+@[simp]
 lemma mulOperator_add_eq
     {μ : Measure (Space d)} (f : Space d → ℂ) {g : Space d → ℂ} (h : (𝓜 μ g).domain = ⊤) :
     𝓜 μ (f + g) = 𝓜 μ f + 𝓜 μ g := by
@@ -395,6 +396,7 @@ lemma mulOperator_sub_ge (μ : Measure (Space d)) (f g : Space d → ℂ) :
     𝓜 μ f - 𝓜 μ g ≤ 𝓜 μ (f - g) :=
   le_of_eq_of_le (by simp [sub_eq_add_neg]) (mulOperator_add_ge μ f (-g))
 
+@[simp]
 lemma mulOperator_sub_eq
     {μ : Measure (Space d)} (f : Space d → ℂ) {g : Space d → ℂ} (h : (𝓜 μ g).domain = ⊤) :
     𝓜 μ (f - g) = 𝓜 μ f - 𝓜 μ g := by