Mul Operator add eq

@[simp]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⟩