1. Physlib
  2. QuantumMechanics
  3. Operators
  4. Multiplication
Imports
/- 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 Physlib.QuantumMechanics.Operators.Unbounded public import Physlib.QuantumMechanics.HilbertSpaces.SpaceD.SchwartzSubmodule

Multiplication operators on SpaceDHilbertSpace

i. Overview

In this module we define and develop the properties of multiplication operators. Given a measure μ on Space d and any function f : Space d → ℂ, the multiplication operator 𝓜 μ f is the partial linear map on SpaceDHilbertSpace d μ with domain {ψ : SpaceDHilbertSpace d μ | MemHS (f • ψ) μ} and mapping ψ to f • ψ. Prime examples of multiplication operators are the position operators which multiply by xᵢ and the potential operators which multiply by the potential function V(x) of a quantum system.

Although the domain of 𝓜 μ f is defined implicitly through MemHS, simple assumptions on f allow one to nail down some of its properties. For example, when f is μ-a.e. strongly measurable then the corresponding multiplication operator is densely defined, if f is μ-a.e. bounded then the domain is ⊤ and if f has temperate growth then the domain contains the Schwartz submodule.

Multiplication operators also form the backbone for derivative operators, which are defined through multiplication in the Fourier domain: see Operators/Derivative.lean.

ii. Key results

    mulOperator μ f (notation 𝓜 μ f) : The operator defined by ψ ↦ f • ψ with maximal domain {ψ : SpaceDHilbertSpace d μ | MemHS (f • ψ) μ}.

    mulOperator_adjoint_eq_conj : The adjoint of 𝓜 μ f is the multiplication operator defined by the conjugate of f.

    mulOperator_isSelfAdjoint : The multiplication operator of a real function is self-adjoint.

    mulOperator_isUnbounded : Multiplication operators with maximal domain are unbounded (i.e. densely defined and closable).

    mulOperator_isClosed : Multiplication operators with maximal domain are closed.

    mulOperator_const_smul_eq : 𝓜 μ (c • f) = c • 𝓜 μ f for non-zero c.

    mulOperator_add_ge / mulOperator_sub_ge : 𝓜 μ (f ± g) is an extension of 𝓜 μ f ± 𝓜 μ g.

    mulOperator_smul_ge : 𝓜 μ (f • g) is an extension of 𝓜 μ f * 𝓜 μ g.

iii. Table of contents

    A. Definition

    B. Domain

    C. Adjoint

      C.1. Self-adjoint

    D. Closed & unbounded

    E. Basic properties

      E.1. Smul & neg

      E.2. Add & sub

      E.3. Composition

    F. Spectrum

iv. References

See examples 1.3 and 3.8 in

    [Konrad Schmüdgen, Unbounded Self-Adjoint Operators on Hilbert Space][Schmudgen2012]

@[expose] public section

A. Definition

The multiplication operator which maps ψ to the equivalence class of f • ψ with maximal domain {ψ : SpaceDHilbertspace d μ | MemHS (f • ψ) μ}.

d:ℕμ:Measure (Space d)f:Space d → ℂc:ℂψ:↥{ carrier := {ψ | MemHS (f • ↑↑ψ) μ}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }⊢ f • ↑↑↑(c • ψ) =ᵐ[μ] (RingHom.id ℂ) c • f • ↑↑↑ψ d:ℕμ:Measure (Space d)f:Space d → ℂc:ℂψ:↥{ carrier := {ψ | MemHS (f • ↑↑ψ) μ}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }⊢ ∀ (a : Space d), ↑↑(c • ↑ψ) a = (c • ↑↑↑ψ) a → (f • ↑↑↑(c • ψ)) a = ((RingHom.id ℂ) c • f • ↑↑↑ψ) a All goals completed! 🐙 }
@[inherit_doc mulOperator] notation "𝓜" => mulOperator

The multiplication operator 𝓜 μ f has maximal domain: ψ is in the domain exactly when multiplying by f gives an element of the Hilbert space.

lemma mem_mulOperator_domain_iff {μ : Measure (Space d)} {f : Space d → ℂ} {ψ : SpaceDHilbertSpace d μ} : ψ ∈ (𝓜 μ f).domain ↔ MemHS (f • ⇑ψ) μ := Iff.rfl

The defining property of a multiplication operator: ψ is mapped to f • ψ.

lemma mulOperator_apply_ae {μ : Measure (Space d)} {f : Space d → ℂ} (ψ : (𝓜 μ f).domain) : 𝓜 μ f ψ =ᵐ[μ] f • ψ := coeFn_mk ψ.prop

B. Domain

The multiplication operator of a μ-a.e. bounded function has full domain.

lemma mulOperator_domain_eq_top {μ : Measure (Space d)} {f : Space d → ℂ} (hf : AEStronglyMeasurable f μ) {c : ℝ} (hfc : ∀ᵐ x ∂μ, ‖f x‖ ≤ c) : (𝓜 μ f).domain = ⊤ := d:ℕμ:Measure (Space d)f:Space d → ℂhf:AEStronglyMeasurable f μc:ℝhfc:∀ᵐ (x : Space d) ∂μ, ‖f x‖ ≤ c⊢ (𝓜 μ f).domain = ⊤ d:ℕμ:Measure (Space d)f:Space d → ℂhf:AEStronglyMeasurable f μc:ℝhfc:∀ᵐ (x : Space d) ∂μ, ‖f x‖ ≤ cψ:↥(SpaceDHilbertSpace d μ)⊢ ψ ∈ (𝓜 μ f).domain refine ((memHS_coe ψ).const_smul c).mono (d:ℕμ:Measure (Space d)f:Space d → ℂhf:AEStronglyMeasurable f μc:ℝhfc:∀ᵐ (x : Space d) ∂μ, ‖f x‖ ≤ cψ:↥(SpaceDHilbertSpace d μ)⊢ AEStronglyMeasurable (f • ↑↑ψ) μ All goals completed! 🐙) ?_ filter_upwards [hfc] with x d:ℕμ:Measure (Space d)f:Space d → ℂhf:AEStronglyMeasurable f μc:ℝhfc:∀ᵐ (x : Space d) ∂μ, ‖f x‖ ≤ cψ:↥(SpaceDHilbertSpace d μ)x:Space dh:‖f x‖ ≤ c⊢ ‖(f • ↑↑ψ) x‖ ≤ ‖(↑c • ↑↑ψ) x‖ d:ℕμ:Measure (Space d)f:Space d → ℂhf:AEStronglyMeasurable f μc:ℝhfc:∀ᵐ (x : Space d) ∂μ, ‖f x‖ ≤ cψ:↥(SpaceDHilbertSpace d μ)x:Space dh:‖f x‖ ≤ c⊢ ‖f x‖ * ‖↑↑ψ x‖ ≤ ‖↑c‖ * ‖↑↑ψ x‖ exact mul_le_mul_of_nonneg_right (h.trans <| d:ℕμ:Measure (Space d)f:Space d → ℂhf:AEStronglyMeasurable f μc:ℝhfc:∀ᵐ (x : Space d) ∂μ, ‖f x‖ ≤ cψ:↥(SpaceDHilbertSpace d μ)x:Space dh:‖f x‖ ≤ c⊢ c ≤ ‖↑c‖ All goals completed! 🐙) (norm_nonneg _)

The domains of multiplication operators shrink with increasing function norm.

lemma mulOperator_domain_antitone {μ : Measure (Space d)} {f g : Space d → ℂ} (hg : AEStronglyMeasurable g μ) (h : ∀ᵐ x ∂μ, ‖g x‖ ≤ ‖f x‖) : (𝓜 μ f).domain ≤ (𝓜 μ g).domain := d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂhg:AEStronglyMeasurable g μh:∀ᵐ (x : Space d) ∂μ, ‖g x‖ ≤ ‖f x‖⊢ (𝓜 μ f).domain ≤ (𝓜 μ g).domain d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂhg:AEStronglyMeasurable g μh:∀ᵐ (x : Space d) ∂μ, ‖g x‖ ≤ ‖f x‖ψ:↥(SpaceDHilbertSpace d μ)hψ:ψ ∈ (𝓜 μ f).domain⊢ ψ ∈ (𝓜 μ g).domain refine hψ.mono (d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂhg:AEStronglyMeasurable g μh:∀ᵐ (x : Space d) ∂μ, ‖g x‖ ≤ ‖f x‖ψ:↥(SpaceDHilbertSpace d μ)hψ:ψ ∈ (𝓜 μ f).domain⊢ AEStronglyMeasurable (g • ↑↑ψ) μ All goals completed! 🐙) ?_ d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂhg:AEStronglyMeasurable g μh:∀ᵐ (x : Space d) ∂μ, ‖g x‖ ≤ ‖f x‖ψ:↥(SpaceDHilbertSpace d μ)hψ:ψ ∈ (𝓜 μ f).domain⊢ ∀ (a : Space d), ‖g a‖ ≤ ‖f a‖ → ‖(g • ↑↑ψ) a‖ ≤ ‖(f • ↑↑ψ) a‖ All goals completed! 🐙

The multiplication operators corresponding to functions of μ-a.e. equal norm have the same domain.

lemma mulOperator_domain_eq_of_congr_norm {μ : Measure (Space d)} {f g : Space d → ℂ} (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) (h : ∀ᵐ x ∂μ, ‖f x‖ = ‖g x‖) : (𝓜 μ f).domain = (𝓜 μ g).domain := d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂhf:AEStronglyMeasurable f μhg:AEStronglyMeasurable g μh:∀ᵐ (x : Space d) ∂μ, ‖f x‖ = ‖g x‖⊢ (𝓜 μ f).domain = (𝓜 μ g).domain d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂhf:AEStronglyMeasurable f μhg:AEStronglyMeasurable g μh:∀ᵐ (x : Space d) ∂μ, ‖f x‖ = ‖g x‖ψ:↥(SpaceDHilbertSpace d μ)⊢ ψ ∈ (𝓜 μ f).domain ↔ ψ ∈ (𝓜 μ g).domain refine memHS_congr_norm (d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂhf:AEStronglyMeasurable f μhg:AEStronglyMeasurable g μh:∀ᵐ (x : Space d) ∂μ, ‖f x‖ = ‖g x‖ψ:↥(SpaceDHilbertSpace d μ)⊢ AEStronglyMeasurable (f • ↑↑ψ) μ All goals completed! 🐙) (d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂhf:AEStronglyMeasurable f μhg:AEStronglyMeasurable g μh:∀ᵐ (x : Space d) ∂μ, ‖f x‖ = ‖g x‖ψ:↥(SpaceDHilbertSpace d μ)⊢ AEStronglyMeasurable (g • ↑↑ψ) μ All goals completed! 🐙) ?_ d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂhf:AEStronglyMeasurable f μhg:AEStronglyMeasurable g μh:∀ᵐ (x : Space d) ∂μ, ‖f x‖ = ‖g x‖ψ:↥(SpaceDHilbertSpace d μ)⊢ ∀ (a : Space d), ‖f a‖ = ‖g a‖ → ‖(f • ↑↑ψ) a‖ = ‖(g • ↑↑ψ) a‖ All goals completed! 🐙

The multiplication operators corresponding to a function and its conjugate have the same domain.

lemma mulOperator_conj_domain {μ : Measure (Space d)} {f : Space d → ℂ} (hf : AEStronglyMeasurable f μ) : (𝓜 μ (conj ∘ f)).domain = (𝓜 μ f).domain := mulOperator_domain_eq_of_congr_norm (d:ℕμ:Measure (Space d)f:Space d → ℂhf:AEStronglyMeasurable f μ⊢ AEStronglyMeasurable (⇑(starRingEnd ℂ) ∘ f) μ All goals completed! 🐙) hf (d:ℕμ:Measure (Space d)f:Space d → ℂhf:AEStronglyMeasurable f μ⊢ ∀ᵐ (x : Space d) ∂μ, ‖(⇑(starRingEnd ℂ) ∘ f) x‖ = ‖f x‖ All goals completed! 🐙)

The multiplication operator corresponding to a μ-a.e. strongly measurable function is densely defined.

d:ℕμ:Measure (Space d)f:Space d → ℂhf:AEStronglyMeasurable f μψ:↥(SpaceDHilbertSpace d μ)u:Space d → ℂhu:Measurable uhfu:f =ᵐ[μ] us:ℕ → Set (Space d) := fun n => u ⁻¹' Metric.closedBall 0 ↑nφ:ℕ → ↥(SpaceDHilbertSpace d μ) := fun n => mk ⋯hφ:∀ (n : ℕ), ↑↑(φ n) =ᵐ[μ] (s n).indicator ↑↑ψh:∀ (n : ℕ), ∫⁻ (x : Space d), ‖↑↑(φ n - ψ) x‖ₑ ^ 2 ∂μ = ∫⁻ (x : Space d), ‖(s n)ᶜ.indicator (↑↑ψ) x‖ₑ ^ 2 ∂μx:Space dn:ℕhn:⌈‖u x‖⌉₊ ≤ n⊢ ‖u x‖ ≤ ↑n exact (Nat.le_ceil _).trans (d:ℕμ:Measure (Space d)f:Space d → ℂhf:AEStronglyMeasurable f μψ:↥(SpaceDHilbertSpace d μ)u:Space d → ℂhu:Measurable uhfu:f =ᵐ[μ] us:ℕ → Set (Space d) := fun n => u ⁻¹' Metric.closedBall 0 ↑nφ:ℕ → ↥(SpaceDHilbertSpace d μ) := fun n => mk ⋯hφ:∀ (n : ℕ), ↑↑(φ n) =ᵐ[μ] (s n).indicator ↑↑ψh:∀ (n : ℕ), ∫⁻ (x : Space d), ‖↑↑(φ n - ψ) x‖ₑ ^ 2 ∂μ = ∫⁻ (x : Space d), ‖(s n)ᶜ.indicator (↑↑ψ) x‖ₑ ^ 2 ∂μx:Space dn:ℕhn:⌈‖u x‖⌉₊ ≤ n⊢ ↑⌈‖u x‖⌉₊ ≤ ↑n All goals completed! 🐙)

C. Adjoint

d:ℕμ:Measure (Space d)inst✝:IsFiniteMeasureOnCompacts μf:Space d → ℂg:Space d → ℂhf:AEStronglyMeasurable f μhg:AEStronglyMeasurable g μw₁:Space d → ℂhw₁:StronglyMeasurable w₁hw₁':(fun x => f x * g x) =ᵐ[μ] w₁w₂:Space d → ℂhw₂:StronglyMeasurable w₂hw₂':(fun x => f x ^ 2 * g x) =ᵐ[μ] w₂s:ℕ → Set (Space d) := fun n => Metric.closedBall 0 ↑n ∩ (w₁ ⁻¹' Metric.closedBall 0 ↑n ∩ w₂ ⁻¹' Metric.closedBall 0 ↑n)k:ℕhk:k = 1 ∨ k = 2n:ℕ⊢ ∫⁻ (a : Space d) in s n, ‖(fun x => ‖f x ^ k * g x‖ ^ 2) a‖ₑ ∂μ ≤ ∫⁻ (x : Space d) in s n, ‖↑n ^ 2‖ₑ ∂μ refine setLIntegral_mono_ae' (d:ℕμ:Measure (Space d)inst✝:IsFiniteMeasureOnCompacts μf:Space d → ℂg:Space d → ℂhf:AEStronglyMeasurable f μhg:AEStronglyMeasurable g μw₁:Space d → ℂhw₁:StronglyMeasurable w₁hw₁':(fun x => f x * g x) =ᵐ[μ] w₁w₂:Space d → ℂhw₂:StronglyMeasurable w₂hw₂':(fun x => f x ^ 2 * g x) =ᵐ[μ] w₂s:ℕ → Set (Space d) := fun n => Metric.closedBall 0 ↑n ∩ (w₁ ⁻¹' Metric.closedBall 0 ↑n ∩ w₂ ⁻¹' Metric.closedBall 0 ↑n)k:ℕhk:k = 1 ∨ k = 2n:ℕ⊢ MeasurableSet (s n) All goals completed! 🐙) ?_ filter_upwards [hw₁', hw₂'] with x d:ℕμ:Measure (Space d)inst✝:IsFiniteMeasureOnCompacts μf:Space d → ℂg:Space d → ℂhf:AEStronglyMeasurable f μhg:AEStronglyMeasurable g μw₁:Space d → ℂhw₁:StronglyMeasurable w₁hw₁':(fun x => f x * g x) =ᵐ[μ] w₁w₂:Space d → ℂhw₂:StronglyMeasurable w₂hw₂':(fun x => f x ^ 2 * g x) =ᵐ[μ] w₂s:ℕ → Set (Space d) := fun n => Metric.closedBall 0 ↑n ∩ (w₁ ⁻¹' Metric.closedBall 0 ↑n ∩ w₂ ⁻¹' Metric.closedBall 0 ↑n)k:ℕhk:k = 1 ∨ k = 2n:ℕx:Space dh₁:f x * g x = w₁ x⊢ f x ^ 2 * g x = w₂ x → x ∈ s n → ‖‖f x ^ k * g x‖ ^ 2‖ₑ ≤ ‖↑n ^ 2‖ₑ d:ℕμ:Measure (Space d)inst✝:IsFiniteMeasureOnCompacts μf:Space d → ℂg:Space d → ℂhf:AEStronglyMeasurable f μhg:AEStronglyMeasurable g μw₁:Space d → ℂhw₁:StronglyMeasurable w₁hw₁':(fun x => f x * g x) =ᵐ[μ] w₁w₂:Space d → ℂhw₂:StronglyMeasurable w₂hw₂':(fun x => f x ^ 2 * g x) =ᵐ[μ] w₂s:ℕ → Set (Space d) := fun n => Metric.closedBall 0 ↑n ∩ (w₁ ⁻¹' Metric.closedBall 0 ↑n ∩ w₂ ⁻¹' Metric.closedBall 0 ↑n)k:ℕhk:k = 1 ∨ k = 2n:ℕx:Space dh₁:f x * g x = w₁ xh₂:f x ^ 2 * g x = w₂ x⊢ x ∈ s n → ‖‖f x ^ k * g x‖ ^ 2‖ₑ ≤ ‖↑n ^ 2‖ₑ d:ℕμ:Measure (Space d)inst✝:IsFiniteMeasureOnCompacts μf:Space d → ℂg:Space d → ℂhf:AEStronglyMeasurable f μhg:AEStronglyMeasurable g μw₁:Space d → ℂhw₁:StronglyMeasurable w₁hw₁':(fun x => f x * g x) =ᵐ[μ] w₁w₂:Space d → ℂhw₂:StronglyMeasurable w₂hw₂':(fun x => f x ^ 2 * g x) =ᵐ[μ] w₂s:ℕ → Set (Space d) := fun n => Metric.closedBall 0 ↑n ∩ (w₁ ⁻¹' Metric.closedBall 0 ↑n ∩ w₂ ⁻¹' Metric.closedBall 0 ↑n)k:ℕhk:k = 1 ∨ k = 2n:ℕx:Space dh₁:f x * g x = w₁ xh₂:f x ^ 2 * g x = w₂ xh₃:x ∈ Metric.closedBall 0 ↑nh₃':x ∈ w₁ ⁻¹' Metric.closedBall 0 ↑n ∩ w₂ ⁻¹' Metric.closedBall 0 ↑n⊢ ‖‖f x ^ k * g x‖ ^ 2‖ₑ ≤ ‖↑n ^ 2‖ₑ d:ℕμ:Measure (Space d)inst✝:IsFiniteMeasureOnCompacts μf:Space d → ℂg:Space d → ℂhf:AEStronglyMeasurable f μhg:AEStronglyMeasurable g μw₁:Space d → ℂhw₁:StronglyMeasurable w₁hw₁':(fun x => f x * g x) =ᵐ[μ] w₁w₂:Space d → ℂhw₂:StronglyMeasurable w₂hw₂':(fun x => f x ^ 2 * g x) =ᵐ[μ] w₂s:ℕ → Set (Space d) := fun n => Metric.closedBall 0 ↑n ∩ (w₁ ⁻¹' Metric.closedBall 0 ↑n ∩ w₂ ⁻¹' Metric.closedBall 0 ↑n)k:ℕhk:k = 1 ∨ k = 2n:ℕx:Space dh₁:f x * g x = w₁ xh₂:f x ^ 2 * g x = w₂ xh₃:x ∈ Metric.closedBall 0 ↑nh₃':x ∈ w₁ ⁻¹' Metric.closedBall 0 ↑n ∩ w₂ ⁻¹' Metric.closedBall 0 ↑n⊢ ‖‖f x ^ k * g x‖ ^ 2‖ ≤ ‖↑n ^ 2‖ simp_rw d:ℕμ:Measure (Space d)inst✝:IsFiniteMeasureOnCompacts μf:Space d → ℂg:Space d → ℂhf:AEStronglyMeasurable f μhg:AEStronglyMeasurable g μw₁:Space d → ℂhw₁:StronglyMeasurable w₁hw₁':(fun x => f x * g x) =ᵐ[μ] w₁w₂:Space d → ℂhw₂:StronglyMeasurable w₂hw₂':(fun x => f x ^ 2 * g x) =ᵐ[μ] w₂s:ℕ → Set (Space d) := fun n => Metric.closedBall 0 ↑n ∩ (w₁ ⁻¹' Metric.closedBall 0 ↑n ∩ w₂ ⁻¹' Metric.closedBall 0 ↑n)k:ℕhk:k = 1 ∨ k = 2n:ℕx:Space dh₁:f x * g x = w₁ xh₂:f x ^ 2 * g x = w₂ xh₃:x ∈ Metric.closedBall 0 ↑nh₃':x ∈ w₁ ⁻¹' Metric.closedBall 0 ↑n ∩ w₂ ⁻¹' Metric.closedBall 0 ↑n⊢ ‖‖f x ^ k * g x‖ ^ 2‖ ≤ ‖↑n ^ 2‖d:ℕμ:Measure (Space d)inst✝:IsFiniteMeasureOnCompacts μf:Space d → ℂg:Space d → ℂhf:AEStronglyMeasurable f μhg:AEStronglyMeasurable g μw₁:Space d → ℂhw₁:StronglyMeasurable w₁hw₁':(fun x => f x * g x) =ᵐ[μ] w₁w₂:Space d → ℂhw₂:StronglyMeasurable w₂hw₂':(fun x => f x ^ 2 * g x) =ᵐ[μ] w₂s:ℕ → Set (Space d) := fun n => Metric.closedBall 0 ↑n ∩ (w₁ ⁻¹' Metric.closedBall 0 ↑n ∩ w₂ ⁻¹' Metric.closedBall 0 ↑n)k:ℕhk:k = 1 ∨ k = 2n:ℕx:Space dh₁:f x * g x = w₁ xh₂:f x ^ 2 * g x = w₂ xh₃:x ∈ Metric.closedBall 0 ↑nh₃':x ∈ w₁ ⁻¹' Metric.closedBall 0 ↑n ∩ w₂ ⁻¹' Metric.closedBall 0 ↑n⊢ ‖‖f x ^ k * g x‖‖ ^ 2 ≤ ‖↑n‖ ^ 2 d:ℕμ:Measure (Space d)inst✝:IsFiniteMeasureOnCompacts μf:Space d → ℂg:Space d → ℂhf:AEStronglyMeasurable f μhg:AEStronglyMeasurable g μw₁:Space d → ℂhw₁:StronglyMeasurable w₁hw₁':(fun x => f x * g x) =ᵐ[μ] w₁w₂:Space d → ℂhw₂:StronglyMeasurable w₂hw₂':(fun x => f x ^ 2 * g x) =ᵐ[μ] w₂s:ℕ → Set (Space d) := fun n => Metric.closedBall 0 ↑n ∩ (w₁ ⁻¹' Metric.closedBall 0 ↑n ∩ w₂ ⁻¹' Metric.closedBall 0 ↑n)k:ℕhk:k = 1 ∨ k = 2n:ℕx:Space dh₁:f x * g x = w₁ xh₂:f x ^ 2 * g x = w₂ xh₃:x ∈ Metric.closedBall 0 ↑nh₃':x ∈ w₁ ⁻¹' Metric.closedBall 0 ↑n ∩ w₂ ⁻¹' Metric.closedBall 0 ↑n⊢ ‖f x ^ k * g x‖ ^ 2 ≤ ‖↑n‖ ^ 2 d:ℕμ:Measure (Space d)inst✝:IsFiniteMeasureOnCompacts μf:Space d → ℂg:Space d → ℂhf:AEStronglyMeasurable f μhg:AEStronglyMeasurable g μw₁:Space d → ℂhw₁:StronglyMeasurable w₁hw₁':(fun x => f x * g x) =ᵐ[μ] w₁w₂:Space d → ℂhw₂:StronglyMeasurable w₂hw₂':(fun x => f x ^ 2 * g x) =ᵐ[μ] w₂s:ℕ → Set (Space d) := fun n => Metric.closedBall 0 ↑n ∩ (w₁ ⁻¹' Metric.closedBall 0 ↑n ∩ w₂ ⁻¹' Metric.closedBall 0 ↑n)k:ℕhk:k = 1 ∨ k = 2n:ℕx:Space dh₁:f x * g x = w₁ xh₂:f x ^ 2 * g x = w₂ xh₃:x ∈ Metric.closedBall 0 ↑nh₃':x ∈ w₁ ⁻¹' Metric.closedBall 0 ↑n ∩ w₂ ⁻¹' Metric.closedBall 0 ↑n⊢ ‖f x ^ k * g x‖ ^ 2 ≤ ↑n ^ 2] d:ℕμ:Measure (Space d)inst✝:IsFiniteMeasureOnCompacts μf:Space d → ℂg:Space d → ℂhf:AEStronglyMeasurable f μhg:AEStronglyMeasurable g μw₁:Space d → ℂhw₁:StronglyMeasurable w₁hw₁':(fun x => f x * g x) =ᵐ[μ] w₁w₂:Space d → ℂhw₂:StronglyMeasurable w₂hw₂':(fun x => f x ^ 2 * g x) =ᵐ[μ] w₂s:ℕ → Set (Space d) := fun n => Metric.closedBall 0 ↑n ∩ (w₁ ⁻¹' Metric.closedBall 0 ↑n ∩ w₂ ⁻¹' Metric.closedBall 0 ↑n)k:ℕhk:k = 1 ∨ k = 2n:ℕx:Space dh₁:f x * g x = w₁ xh₂:f x ^ 2 * g x = w₂ xh₃:x ∈ Metric.closedBall 0 ↑nh₃':x ∈ w₁ ⁻¹' Metric.closedBall 0 ↑n ∩ w₂ ⁻¹' Metric.closedBall 0 ↑n⊢ ‖f x ^ k * g x‖ ≤ ↑n d:ℕμ:Measure (Space d)inst✝:IsFiniteMeasureOnCompacts μf:Space d → ℂg:Space d → ℂhf:AEStronglyMeasurable f μhg:AEStronglyMeasurable g μw₁:Space d → ℂhw₁:StronglyMeasurable w₁hw₁':(fun x => f x * g x) =ᵐ[μ] w₁w₂:Space d → ℂhw₂:StronglyMeasurable w₂hw₂':(fun x => f x ^ 2 * g x) =ᵐ[μ] w₂s:ℕ → Set (Space d) := fun n => Metric.closedBall 0 ↑n ∩ (w₁ ⁻¹' Metric.closedBall 0 ↑n ∩ w₂ ⁻¹' Metric.closedBall 0 ↑n)k:ℕn:ℕx:Space dh₁:f x * g x = w₁ xh₂:f x ^ 2 * g x = w₂ xh₃:x ∈ Metric.closedBall 0 ↑nh₃':x ∈ w₁ ⁻¹' Metric.closedBall 0 ↑n ∩ w₂ ⁻¹' Metric.closedBall 0 ↑nh✝:k = 1⊢ ‖f x ^ k * g x‖ ≤ ↑nd:ℕμ:Measure (Space d)inst✝:IsFiniteMeasureOnCompacts μf:Space d → ℂg:Space d → ℂhf:AEStronglyMeasurable f μhg:AEStronglyMeasurable g μw₁:Space d → ℂhw₁:StronglyMeasurable w₁hw₁':(fun x => f x * g x) =ᵐ[μ] w₁w₂:Space d → ℂhw₂:StronglyMeasurable w₂hw₂':(fun x => f x ^ 2 * g x) =ᵐ[μ] w₂s:ℕ → Set (Space d) := fun n => Metric.closedBall 0 ↑n ∩ (w₁ ⁻¹' Metric.closedBall 0 ↑n ∩ w₂ ⁻¹' Metric.closedBall 0 ↑n)k:ℕn:ℕx:Space dh₁:f x * g x = w₁ xh₂:f x ^ 2 * g x = w₂ xh₃:x ∈ Metric.closedBall 0 ↑nh₃':x ∈ w₁ ⁻¹' Metric.closedBall 0 ↑n ∩ w₂ ⁻¹' Metric.closedBall 0 ↑nh✝:k = 2⊢ ‖f x ^ k * g x‖ ≤ ↑n d:ℕμ:Measure (Space d)inst✝:IsFiniteMeasureOnCompacts μf:Space d → ℂg:Space d → ℂhf:AEStronglyMeasurable f μhg:AEStronglyMeasurable g μw₁:Space d → ℂhw₁:StronglyMeasurable w₁hw₁':(fun x => f x * g x) =ᵐ[μ] w₁w₂:Space d → ℂhw₂:StronglyMeasurable w₂hw₂':(fun x => f x ^ 2 * g x) =ᵐ[μ] w₂s:ℕ → Set (Space d) := fun n => Metric.closedBall 0 ↑n ∩ (w₁ ⁻¹' Metric.closedBall 0 ↑n ∩ w₂ ⁻¹' Metric.closedBall 0 ↑n)k:ℕn:ℕx:Space dh₁:f x * g x = w₁ xh₂:f x ^ 2 * g x = w₂ xh₃:x ∈ Metric.closedBall 0 ↑nh₃':x ∈ w₁ ⁻¹' Metric.closedBall 0 ↑n ∩ w₂ ⁻¹' Metric.closedBall 0 ↑nh✝:k = 1⊢ ‖f x ^ k * g x‖ ≤ ↑nd:ℕμ:Measure (Space d)inst✝:IsFiniteMeasureOnCompacts μf:Space d → ℂg:Space d → ℂhf:AEStronglyMeasurable f μhg:AEStronglyMeasurable g μw₁:Space d → ℂhw₁:StronglyMeasurable w₁hw₁':(fun x => f x * g x) =ᵐ[μ] w₁w₂:Space d → ℂhw₂:StronglyMeasurable w₂hw₂':(fun x => f x ^ 2 * g x) =ᵐ[μ] w₂s:ℕ → Set (Space d) := fun n => Metric.closedBall 0 ↑n ∩ (w₁ ⁻¹' Metric.closedBall 0 ↑n ∩ w₂ ⁻¹' Metric.closedBall 0 ↑n)k:ℕn:ℕx:Space dh₁:f x * g x = w₁ xh₂:f x ^ 2 * g x = w₂ xh₃:x ∈ Metric.closedBall 0 ↑nh₃':x ∈ w₁ ⁻¹' Metric.closedBall 0 ↑n ∩ w₂ ⁻¹' Metric.closedBall 0 ↑nh✝:k = 2⊢ ‖f x ^ k * g x‖ ≤ ↑n All goals completed! 🐙 d:ℕμ:Measure (Space d)inst✝:IsFiniteMeasureOnCompacts μf:Space d → ℂg:Space d → ℂhf:AEStronglyMeasurable f μhg:AEStronglyMeasurable g μw₁:Space d → ℂhw₁:StronglyMeasurable w₁hw₁':(fun x => f x * g x) =ᵐ[μ] w₁w₂:Space d → ℂhw₂:StronglyMeasurable w₂hw₂':(fun x => f x ^ 2 * g x) =ᵐ[μ] w₂s:ℕ → Set (Space d) := fun n => Metric.closedBall 0 ↑n ∩ (w₁ ⁻¹' Metric.closedBall 0 ↑n ∩ w₂ ⁻¹' Metric.closedBall 0 ↑n)k:ℕhk:k = 1 ∨ k = 2n:ℕ⊢ ‖↑n ^ 2‖ₑ * μ (s n) < ⊤ refine ENNReal.mul_lt_top (d:ℕμ:Measure (Space d)inst✝:IsFiniteMeasureOnCompacts μf:Space d → ℂg:Space d → ℂhf:AEStronglyMeasurable f μhg:AEStronglyMeasurable g μw₁:Space d → ℂhw₁:StronglyMeasurable w₁hw₁':(fun x => f x * g x) =ᵐ[μ] w₁w₂:Space d → ℂhw₂:StronglyMeasurable w₂hw₂':(fun x => f x ^ 2 * g x) =ᵐ[μ] w₂s:ℕ → Set (Space d) := fun n => Metric.closedBall 0 ↑n ∩ (w₁ ⁻¹' Metric.closedBall 0 ↑n ∩ w₂ ⁻¹' Metric.closedBall 0 ↑n)k:ℕhk:k = 1 ∨ k = 2n:ℕ⊢ ‖↑n ^ 2‖ₑ < ⊤ All goals completed! 🐙) ?_ All goals completed! 🐙

The adjoint of a multiplication operator is again a multiplication operator.

All goals completed! 🐙

C.1. Self-adjoint

The multiplication operator corresponding to a real function is self-adjoint.

All goals completed! 🐙

D. Closed & unbounded

Multiplication operators of μ-a.e. strongly measurable functions are closable.

lemma mulOperator_isClosable {μ : Measure (Space d)} [IsFiniteMeasureOnCompacts μ] {f : Space d → ℂ} (hf : AEStronglyMeasurable f μ) : (𝓜 μ f).IsClosable := d:ℕμ:Measure (Space d)inst✝:IsFiniteMeasureOnCompacts μf:Space d → ℂhf:AEStronglyMeasurable f μ⊢ (𝓜 μ f).IsClosable d:ℕμ:Measure (Space d)inst✝:IsFiniteMeasureOnCompacts μf:Space d → ℂhf:AEStronglyMeasurable f μ⊢ ∃ U', U'.HasDenseDomain ∧ U'.IsFormalAdjoint (𝓜 μ f) exact ⟨𝓜 μ (conj ∘ f), mulOperator_hasDenseDomain (d:ℕμ:Measure (Space d)inst✝:IsFiniteMeasureOnCompacts μf:Space d → ℂhf:AEStronglyMeasurable f μ⊢ AEStronglyMeasurable (⇑(starRingEnd ℂ) ∘ f) μ All goals completed! 🐙), mulOperator_adjoint_eq_conj hf ▸ adjoint_isFormalAdjoint (mulOperator_hasDenseDomain hf)⟩

Multiplication operators of μ-a.e. strongly measurable functions are unbounded.

lemma mulOperator_isUnbounded {μ : Measure (Space d)} [IsFiniteMeasureOnCompacts μ] {f : Space d → ℂ} (hf : AEStronglyMeasurable f μ) : (𝓜 μ f).IsUnbounded := ⟨mulOperator_hasDenseDomain hf, mulOperator_isClosable hf⟩

Multiplication operators of μ-a.e. strongly measurable functions are closed.

d:ℕμ:Measure (Space d)inst✝:IsFiniteMeasureOnCompacts μf:Space d → ℂhf:AEStronglyMeasurable f μ⊢ 𝓜 μ (⇑(starRingEnd ℂ) ∘ ⇑(starRingEnd ℂ) ∘ f) = 𝓜 μ f d:ℕμ:Measure (Space d)inst✝:IsFiniteMeasureOnCompacts μf:Space d → ℂhf:AEStronglyMeasurable f μ⊢ ⇑(starRingEnd ℂ) ∘ ⇑(starRingEnd ℂ) ∘ f = f; d:ℕμ:Measure (Space d)inst✝:IsFiniteMeasureOnCompacts μf:Space d → ℂhf:AEStronglyMeasurable f μx✝:Space d⊢ (⇑(starRingEnd ℂ) ∘ ⇑(starRingEnd ℂ) ∘ f) x✝ = f x✝; All goals completed! 🐙

E. Basic properties

The multiplication operator of the zero function is the zero operator (domain ⊤).

@[simp] lemma mulOperator_zero (μ : Measure (Space d)) : 𝓜 μ 0 = 0 := d:ℕμ:Measure (Space d)⊢ 𝓜 μ 0 = 0 d:ℕμ:Measure (Space d)ψ:↥(SpaceDHilbertSpace d μ)⊢ ψ ∈ (𝓜 μ 0).domain ↔ ψ ∈ domain 0d:ℕμ:Measure (Space d)ψ:↥(SpaceDHilbertSpace d μ)hψ:ψ ∈ (𝓜 μ 0).domainhψ':ψ ∈ domain 0⊢ ↑↑(↑(𝓜 μ 0) ⟨ψ, hψ⟩) =ᵐ[μ] ↑↑(↑0 ⟨ψ, hψ'⟩) d:ℕμ:Measure (Space d)ψ:↥(SpaceDHilbertSpace d μ)⊢ ψ ∈ (𝓜 μ 0).domain ↔ ψ ∈ domain 0 All goals completed! 🐙 d:ℕμ:Measure (Space d)ψ:↥(SpaceDHilbertSpace d μ)hψ:ψ ∈ (𝓜 μ 0).domainhψ':ψ ∈ domain 0⊢ ↑↑(↑(𝓜 μ 0) ⟨ψ, hψ⟩) =ᵐ[μ] ↑↑(↑0 ⟨ψ, hψ'⟩) d:ℕμ:Measure (Space d)ψ:↥(SpaceDHilbertSpace d μ)hψ:ψ ∈ (𝓜 μ 0).domainhψ':ψ ∈ domain 0⊢ 0 • ↑↑↑⟨ψ, hψ⟩ =ᵐ[μ] ↑↑(↑0 ⟨ψ, hψ'⟩) All goals completed! 🐙

μ-a.e. equal functions give rise to the same multiplication operator.

lemma mulOperator_eq_of_congr_ae {μ : Measure (Space d)} {f g : Space d → ℂ} (h : f =ᵐ[μ] g) : 𝓜 μ f = 𝓜 μ g := d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂh:f =ᵐ[μ] g⊢ 𝓜 μ f = 𝓜 μ g d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂh:f =ᵐ[μ] gψ:↥(SpaceDHilbertSpace d μ)⊢ ψ ∈ (𝓜 μ f).domain ↔ ψ ∈ (𝓜 μ g).domaind:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂh:f =ᵐ[μ] gψ:↥(SpaceDHilbertSpace d μ)hψ:ψ ∈ (𝓜 μ f).domainhψ':ψ ∈ (𝓜 μ g).domain⊢ ↑↑(↑(𝓜 μ f) ⟨ψ, hψ⟩) =ᵐ[μ] ↑↑(↑(𝓜 μ g) ⟨ψ, hψ'⟩) d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂh:f =ᵐ[μ] gψ:↥(SpaceDHilbertSpace d μ)⊢ ψ ∈ (𝓜 μ f).domain ↔ ψ ∈ (𝓜 μ g).domain All goals completed! 🐙 d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂh:f =ᵐ[μ] gψ:↥(SpaceDHilbertSpace d μ)hψ:ψ ∈ (𝓜 μ f).domainhψ':ψ ∈ (𝓜 μ g).domain⊢ ↑↑(↑(𝓜 μ f) ⟨ψ, hψ⟩) =ᵐ[μ] ↑↑(↑(𝓜 μ g) ⟨ψ, hψ'⟩) d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂh:f =ᵐ[μ] gψ:↥(SpaceDHilbertSpace d μ)hψ:ψ ∈ (𝓜 μ f).domainhψ':ψ ∈ (𝓜 μ g).domain⊢ ∀ (a : Space d), f a = g a → ↑↑(↑(𝓜 μ f) ⟨ψ, hψ⟩) a = (f • ↑↑ψ) a → ↑↑(↑(𝓜 μ g) ⟨ψ, hψ'⟩) a = (g • ↑↑ψ) a → ↑↑(↑(𝓜 μ f) ⟨ψ, hψ⟩) a = ↑↑(↑(𝓜 μ g) ⟨ψ, hψ'⟩) a All goals completed! 🐙
TODO "Upgrade mulOperator_eq_of_congr_ae to an iff : 𝓜 μ f = 𝓜 μ g ↔ f =ᵐ[μ] g."

E.1. Smul & neg

Scalar multiplication and mulOperator commute except possibly for c = 0 where the domains of 0 • 𝓜 μ f and 𝓜 μ 0 = 0 may not agree.

See mulOperator_const_smul_eq for equality when c ≠ 0.

d:ℕμ:Measure (Space d)f:Space d → ℂc:ℂu:↥(SpaceDHilbertSpace d μ) × ↥(SpaceDHilbertSpace d μ)v:↥(SpaceDHilbertSpace d μ)hv:v ∈ (c • 𝓜 μ f).domainhvu:↑⟨v, hv⟩ = u.1hvu':↑(c • 𝓜 μ f) ⟨v, hv⟩ = u.2hv':v ∈ (𝓜 μ (c • f)).domain⊢ ↑↑(↑(𝓜 μ (c • f)) ⟨v, hv'⟩) =ᵐ[μ] ↑↑(↑(c • 𝓜 μ f) ⟨v, hv⟩) d:ℕμ:Measure (Space d)f:Space d → ℂc:ℂu:↥(SpaceDHilbertSpace d μ) × ↥(SpaceDHilbertSpace d μ)v:↥(SpaceDHilbertSpace d μ)hv:v ∈ (c • 𝓜 μ f).domainhvu:↑⟨v, hv⟩ = u.1hvu':↑(c • 𝓜 μ f) ⟨v, hv⟩ = u.2hv':v ∈ (𝓜 μ (c • f)).domain⊢ ∀ (a : Space d), ↑↑(↑(𝓜 μ f) ⟨v, hv⟩) a = (f • ↑↑v) a → ↑↑(↑(𝓜 μ (c • f)) ⟨v, hv'⟩) a = ((c • f) • ↑↑v) a → ↑↑(c • ↑(𝓜 μ f) ⟨v, hv⟩) a = (c • ↑↑(↑(𝓜 μ f) ⟨v, hv⟩)) a → ↑↑(↑(𝓜 μ (c • f)) ⟨v, hv'⟩) a = ↑↑(↑(c • 𝓜 μ f) ⟨v, hv⟩) a All goals completed! 🐙

Scalar multiplication and mulOperator commute for c ≠ 0.

@[simp] lemma mulOperator_const_smul_eq (μ : Measure (Space d)) (f : Space d → ℂ) {c : ℂ} (hc : c ≠ 0) : 𝓜 μ (c • f) = c • 𝓜 μ f := d:ℕμ:Measure (Space d)f:Space d → ℂc:ℂhc:c ≠ 0⊢ 𝓜 μ (c • f) = c • 𝓜 μ f d:ℕμ:Measure (Space d)f:Space d → ℂc:ℂhc:c ≠ 0⊢ (c • 𝓜 μ f).domain = (𝓜 μ (c • f)).domain d:ℕμ:Measure (Space d)f:Space d → ℂc:ℂhc:c ≠ 0x✝:↥(SpaceDHilbertSpace d μ)⊢ x✝ ∈ (c • 𝓜 μ f).domain ↔ x✝ ∈ (𝓜 μ (c • f)).domain All goals completed! 🐙

Negation and mulOperator commute.

All goals completed! 🐙

E.2. Add & sub

𝓜 μ (f + g) extends 𝓜 μ f + 𝓜 μ g.

In general the domains do not match: ψ ∈ (𝓜 μ f + 𝓜 μ g).domain amounts to MemHS (f • ψ) μ and MemHS (g • ψ) μ whereas ψ ∈ (𝓜 μ (f + g)).domain is equivalent to the weaker condition MemHS ((f + g) • ψ) μ.

See mulOperator_add_eq and mulOperator_add_eq' for sufficient conditions to ensure equality.

d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂu:↥(SpaceDHilbertSpace d μ) × ↥(SpaceDHilbertSpace d μ)v:↥(SpaceDHilbertSpace d μ)hv:v ∈ (𝓜 μ f + 𝓜 μ g).domainhvu:↑⟨v, hv⟩ = u.1hvu':↑(𝓜 μ f + 𝓜 μ g) ⟨v, hv⟩ = u.2hv':v ∈ (𝓜 μ (f + g)).domain⊢ ↑↑(↑(𝓜 μ (f + g)) ⟨v, hv'⟩) =ᵐ[μ] ↑↑(↑(𝓜 μ f + 𝓜 μ g) ⟨v, hv⟩) d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂu:↥(SpaceDHilbertSpace d μ) × ↥(SpaceDHilbertSpace d μ)v:↥(SpaceDHilbertSpace d μ)hv:v ∈ (𝓜 μ f + 𝓜 μ g).domainhvu:↑⟨v, hv⟩ = u.1hvu':↑(𝓜 μ f + 𝓜 μ g) ⟨v, hv⟩ = u.2hv':v ∈ (𝓜 μ (f + g)).domain⊢ ↑↑(↑(𝓜 μ (f + g)) ⟨v, hv'⟩) =ᵐ[μ] ↑↑(↑(𝓜 μ f) ⟨v, ⋯⟩ + ↑(𝓜 μ g) ⟨v, ⋯⟩) d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂu:↥(SpaceDHilbertSpace d μ) × ↥(SpaceDHilbertSpace d μ)v:↥(SpaceDHilbertSpace d μ)hv:v ∈ (𝓜 μ f + 𝓜 μ g).domainhvu:↑⟨v, hv⟩ = u.1hvu':↑(𝓜 μ f + 𝓜 μ g) ⟨v, hv⟩ = u.2hv':v ∈ (𝓜 μ (f + g)).domain⊢ ∀ (a : Space d), ↑↑(↑(𝓜 μ f) ⟨v, ⋯⟩) a = (f • ↑↑v) a → ↑↑(↑(𝓜 μ g) ⟨v, ⋯⟩) a = (g • ↑↑v) a → ↑↑(↑(𝓜 μ (f + g)) ⟨v, hv'⟩) a = ((f + g) • ↑↑v) a → ↑(↑(↑(𝓜 μ f) ⟨v, ⋯⟩) + ↑(↑(𝓜 μ g) ⟨v, ⋯⟩)) a = (↑↑(↑(𝓜 μ f) ⟨v, ⋯⟩) + ↑↑(↑(𝓜 μ g) ⟨v, ⋯⟩)) a → ↑↑(↑(𝓜 μ (f + g)) ⟨v, hv'⟩) a = ↑↑(↑(𝓜 μ f) ⟨v, ⋯⟩ + ↑(𝓜 μ g) ⟨v, ⋯⟩) a All goals completed! 🐙

(𝓜 μ g).domain = ⊤ is a sufficient condition to ensure equality in mulOperator_add_ge.

d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂh:(𝓜 μ g).domain = ⊤hle:𝓜 μ f + 𝓜 μ g ≤ 𝓜 μ (f + g)ψ:↥(SpaceDHilbertSpace d μ)hψ:ψ ∈ (𝓜 μ (f + g)).domainhg:ψ ∈ (𝓜 μ g).domain⊢ ψ ∈ (𝓜 μ f + 𝓜 μ g).domain d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂh:(𝓜 μ g).domain = ⊤hle:𝓜 μ f + 𝓜 μ g ≤ 𝓜 μ (f + g)ψ:↥(SpaceDHilbertSpace d μ)hψ:MemHS ((f + g) • ↑↑ψ) μhg:MemHS (g • ↑↑ψ) μ⊢ MemHS (f • ↑↑ψ) μ ∧ MemHS (g • ↑↑ψ) μ exact ⟨d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂh:(𝓜 μ g).domain = ⊤hle:𝓜 μ f + 𝓜 μ g ≤ 𝓜 μ (f + g)ψ:↥(SpaceDHilbertSpace d μ)hψ:MemHS ((f + g) • ↑↑ψ) μhg:MemHS (g • ↑↑ψ) μ⊢ MemHS (f • ↑↑ψ) μ All goals completed! 🐙, hg⟩

Having both ‖f x‖ ≤ c * ‖f x + g x‖ and ‖g x‖ ≤ c' * ‖f x + g x‖ μ-a.e. is a sufficient condition to ensure equality in mulOperator_add_ge.

lemma mulOperator_add_eq' {μ : Measure (Space d)} {f g : Space d → ℂ} (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) (c c' : ℝ) (hf' : ∀ᵐ x ∂μ, ‖f x‖ ≤ c * ‖f x + g x‖) (hg' : ∀ᵐ x ∂μ, ‖g x‖ ≤ c' * ‖f x + g x‖) : 𝓜 μ (f + g) = 𝓜 μ f + 𝓜 μ g := d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂhf:AEStronglyMeasurable f μhg:AEStronglyMeasurable g μc:ℝc':ℝhf':∀ᵐ (x : Space d) ∂μ, ‖f x‖ ≤ c * ‖f x + g x‖hg':∀ᵐ (x : Space d) ∂μ, ‖g x‖ ≤ c' * ‖f x + g x‖⊢ 𝓜 μ (f + g) = 𝓜 μ f + 𝓜 μ g d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂhf:AEStronglyMeasurable f μhg:AEStronglyMeasurable g μc:ℝc':ℝhf':∀ᵐ (x : Space d) ∂μ, ‖f x‖ ≤ c * ‖f x + g x‖hg':∀ᵐ (x : Space d) ∂μ, ‖g x‖ ≤ c' * ‖f x + g x‖hle:𝓜 μ f + 𝓜 μ g ≤ 𝓜 μ (f + g)⊢ 𝓜 μ (f + g) = 𝓜 μ f + 𝓜 μ g d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂhf:AEStronglyMeasurable f μhg:AEStronglyMeasurable g μc:ℝc':ℝhf':∀ᵐ (x : Space d) ∂μ, ‖f x‖ ≤ c * ‖f x + g x‖hg':∀ᵐ (x : Space d) ∂μ, ‖g x‖ ≤ c' * ‖f x + g x‖hle:𝓜 μ f + 𝓜 μ g ≤ 𝓜 μ (f + g)⊢ (𝓜 μ f + 𝓜 μ g).domain = (𝓜 μ (f + g)).domain d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂhf:AEStronglyMeasurable f μhg:AEStronglyMeasurable g μc:ℝc':ℝhf':∀ᵐ (x : Space d) ∂μ, ‖f x‖ ≤ c * ‖f x + g x‖hg':∀ᵐ (x : Space d) ∂μ, ‖g x‖ ≤ c' * ‖f x + g x‖hle:𝓜 μ f + 𝓜 μ g ≤ 𝓜 μ (f + g)ψ:↥(SpaceDHilbertSpace d μ)hψ:ψ ∈ (𝓜 μ (f + g)).domain⊢ ψ ∈ ↑(𝓜 μ f).domaind:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂhf:AEStronglyMeasurable f μhg:AEStronglyMeasurable g μc:ℝc':ℝhf':∀ᵐ (x : Space d) ∂μ, ‖f x‖ ≤ c * ‖f x + g x‖hg':∀ᵐ (x : Space d) ∂μ, ‖g x‖ ≤ c' * ‖f x + g x‖hle:𝓜 μ f + 𝓜 μ g ≤ 𝓜 μ (f + g)ψ:↥(SpaceDHilbertSpace d μ)hψ:ψ ∈ (𝓜 μ (f + g)).domain⊢ ψ ∈ ↑(𝓜 μ g).domain d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂhf:AEStronglyMeasurable f μhg:AEStronglyMeasurable g μc:ℝc':ℝhf':∀ᵐ (x : Space d) ∂μ, ‖f x‖ ≤ c * ‖f x + g x‖hg':∀ᵐ (x : Space d) ∂μ, ‖g x‖ ≤ c' * ‖f x + g x‖hle:𝓜 μ f + 𝓜 μ g ≤ 𝓜 μ (f + g)ψ:↥(SpaceDHilbertSpace d μ)hψ:ψ ∈ (𝓜 μ (f + g)).domain⊢ ψ ∈ ↑(𝓜 μ f).domain refine (hψ.const_smul c).mono (d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂhf:AEStronglyMeasurable f μhg:AEStronglyMeasurable g μc:ℝc':ℝhf':∀ᵐ (x : Space d) ∂μ, ‖f x‖ ≤ c * ‖f x + g x‖hg':∀ᵐ (x : Space d) ∂μ, ‖g x‖ ≤ c' * ‖f x + g x‖hle:𝓜 μ f + 𝓜 μ g ≤ 𝓜 μ (f + g)ψ:↥(SpaceDHilbertSpace d μ)hψ:ψ ∈ (𝓜 μ (f + g)).domain⊢ AEStronglyMeasurable (f • ↑↑ψ) μ All goals completed! 🐙) ?_ filter_upwards [hf'] with x d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂhf:AEStronglyMeasurable f μhg:AEStronglyMeasurable g μc:ℝc':ℝhf':∀ᵐ (x : Space d) ∂μ, ‖f x‖ ≤ c * ‖f x + g x‖hg':∀ᵐ (x : Space d) ∂μ, ‖g x‖ ≤ c' * ‖f x + g x‖hle:𝓜 μ f + 𝓜 μ g ≤ 𝓜 μ (f + g)ψ:↥(SpaceDHilbertSpace d μ)hψ:ψ ∈ (𝓜 μ (f + g)).domainx:Space dh:‖f x‖ ≤ c * ‖f x + g x‖⊢ ‖(f • ↑↑ψ) x‖ ≤ ‖(↑c • (f + g) • ↑↑ψ) x‖ d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂhf:AEStronglyMeasurable f μhg:AEStronglyMeasurable g μc:ℝc':ℝhf':∀ᵐ (x : Space d) ∂μ, ‖f x‖ ≤ c * ‖f x + g x‖hg':∀ᵐ (x : Space d) ∂μ, ‖g x‖ ≤ c' * ‖f x + g x‖hle:𝓜 μ f + 𝓜 μ g ≤ 𝓜 μ (f + g)ψ:↥(SpaceDHilbertSpace d μ)hψ:ψ ∈ (𝓜 μ (f + g)).domainx:Space dh:‖f x‖ ≤ c * ‖f x + g x‖⊢ ‖(f • ↑↑ψ) x‖ ≤ c * (‖f x + g x‖ * ‖↑↑ψ x‖)d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂhf:AEStronglyMeasurable f μhg:AEStronglyMeasurable g μc:ℝc':ℝhf':∀ᵐ (x : Space d) ∂μ, ‖f x‖ ≤ c * ‖f x + g x‖hg':∀ᵐ (x : Space d) ∂μ, ‖g x‖ ≤ c' * ‖f x + g x‖hle:𝓜 μ f + 𝓜 μ g ≤ 𝓜 μ (f + g)ψ:↥(SpaceDHilbertSpace d μ)hψ:ψ ∈ (𝓜 μ (f + g)).domainx:Space dh:‖f x‖ ≤ c * ‖f x + g x‖⊢ c * (‖f x + g x‖ * ‖↑↑ψ x‖) ≤ ‖(↑c • (f + g) • ↑↑ψ) x‖ d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂhf:AEStronglyMeasurable f μhg:AEStronglyMeasurable g μc:ℝc':ℝhf':∀ᵐ (x : Space d) ∂μ, ‖f x‖ ≤ c * ‖f x + g x‖hg':∀ᵐ (x : Space d) ∂μ, ‖g x‖ ≤ c' * ‖f x + g x‖hle:𝓜 μ f + 𝓜 μ g ≤ 𝓜 μ (f + g)ψ:↥(SpaceDHilbertSpace d μ)hψ:ψ ∈ (𝓜 μ (f + g)).domainx:Space dh:‖f x‖ ≤ c * ‖f x + g x‖⊢ ‖(f • ↑↑ψ) x‖ ≤ c * (‖f x + g x‖ * ‖↑↑ψ x‖) All goals completed! 🐙 d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂhf:AEStronglyMeasurable f μhg:AEStronglyMeasurable g μc:ℝc':ℝhf':∀ᵐ (x : Space d) ∂μ, ‖f x‖ ≤ c * ‖f x + g x‖hg':∀ᵐ (x : Space d) ∂μ, ‖g x‖ ≤ c' * ‖f x + g x‖hle:𝓜 μ f + 𝓜 μ g ≤ 𝓜 μ (f + g)ψ:↥(SpaceDHilbertSpace d μ)hψ:ψ ∈ (𝓜 μ (f + g)).domainx:Space dh:‖f x‖ ≤ c * ‖f x + g x‖⊢ c * (‖f x + g x‖ * ‖↑↑ψ x‖) ≤ ‖(↑c • (f + g) • ↑↑ψ) x‖ exact le_of_le_of_eq (mul_le_mul_of_nonneg_right (le_abs_self c) (d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂhf:AEStronglyMeasurable f μhg:AEStronglyMeasurable g μc:ℝc':ℝhf':∀ᵐ (x : Space d) ∂μ, ‖f x‖ ≤ c * ‖f x + g x‖hg':∀ᵐ (x : Space d) ∂μ, ‖g x‖ ≤ c' * ‖f x + g x‖hle:𝓜 μ f + 𝓜 μ g ≤ 𝓜 μ (f + g)ψ:↥(SpaceDHilbertSpace d μ)hψ:ψ ∈ (𝓜 μ (f + g)).domainx:Space dh:‖f x‖ ≤ c * ‖f x + g x‖⊢ 0 ≤ ‖f x + g x‖ * ‖↑↑ψ x‖ All goals completed! 🐙)) (d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂhf:AEStronglyMeasurable f μhg:AEStronglyMeasurable g μc:ℝc':ℝhf':∀ᵐ (x : Space d) ∂μ, ‖f x‖ ≤ c * ‖f x + g x‖hg':∀ᵐ (x : Space d) ∂μ, ‖g x‖ ≤ c' * ‖f x + g x‖hle:𝓜 μ f + 𝓜 μ g ≤ 𝓜 μ (f + g)ψ:↥(SpaceDHilbertSpace d μ)hψ:ψ ∈ (𝓜 μ (f + g)).domainx:Space dh:‖f x‖ ≤ c * ‖f x + g x‖⊢ |c| * (‖f x + g x‖ * ‖↑↑ψ x‖) = ‖(↑c • (f + g) • ↑↑ψ) x‖ All goals completed! 🐙) d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂhf:AEStronglyMeasurable f μhg:AEStronglyMeasurable g μc:ℝc':ℝhf':∀ᵐ (x : Space d) ∂μ, ‖f x‖ ≤ c * ‖f x + g x‖hg':∀ᵐ (x : Space d) ∂μ, ‖g x‖ ≤ c' * ‖f x + g x‖hle:𝓜 μ f + 𝓜 μ g ≤ 𝓜 μ (f + g)ψ:↥(SpaceDHilbertSpace d μ)hψ:ψ ∈ (𝓜 μ (f + g)).domain⊢ ψ ∈ ↑(𝓜 μ g).domain refine (hψ.const_smul c').mono (d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂhf:AEStronglyMeasurable f μhg:AEStronglyMeasurable g μc:ℝc':ℝhf':∀ᵐ (x : Space d) ∂μ, ‖f x‖ ≤ c * ‖f x + g x‖hg':∀ᵐ (x : Space d) ∂μ, ‖g x‖ ≤ c' * ‖f x + g x‖hle:𝓜 μ f + 𝓜 μ g ≤ 𝓜 μ (f + g)ψ:↥(SpaceDHilbertSpace d μ)hψ:ψ ∈ (𝓜 μ (f + g)).domain⊢ AEStronglyMeasurable (g • ↑↑ψ) μ All goals completed! 🐙) ?_ filter_upwards [hg'] with x d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂhf:AEStronglyMeasurable f μhg:AEStronglyMeasurable g μc:ℝc':ℝhf':∀ᵐ (x : Space d) ∂μ, ‖f x‖ ≤ c * ‖f x + g x‖hg':∀ᵐ (x : Space d) ∂μ, ‖g x‖ ≤ c' * ‖f x + g x‖hle:𝓜 μ f + 𝓜 μ g ≤ 𝓜 μ (f + g)ψ:↥(SpaceDHilbertSpace d μ)hψ:ψ ∈ (𝓜 μ (f + g)).domainx:Space dh:‖g x‖ ≤ c' * ‖f x + g x‖⊢ ‖(g • ↑↑ψ) x‖ ≤ ‖(↑c' • (f + g) • ↑↑ψ) x‖ d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂhf:AEStronglyMeasurable f μhg:AEStronglyMeasurable g μc:ℝc':ℝhf':∀ᵐ (x : Space d) ∂μ, ‖f x‖ ≤ c * ‖f x + g x‖hg':∀ᵐ (x : Space d) ∂μ, ‖g x‖ ≤ c' * ‖f x + g x‖hle:𝓜 μ f + 𝓜 μ g ≤ 𝓜 μ (f + g)ψ:↥(SpaceDHilbertSpace d μ)hψ:ψ ∈ (𝓜 μ (f + g)).domainx:Space dh:‖g x‖ ≤ c' * ‖f x + g x‖⊢ ‖(g • ↑↑ψ) x‖ ≤ c' * (‖f x + g x‖ * ‖↑↑ψ x‖)d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂhf:AEStronglyMeasurable f μhg:AEStronglyMeasurable g μc:ℝc':ℝhf':∀ᵐ (x : Space d) ∂μ, ‖f x‖ ≤ c * ‖f x + g x‖hg':∀ᵐ (x : Space d) ∂μ, ‖g x‖ ≤ c' * ‖f x + g x‖hle:𝓜 μ f + 𝓜 μ g ≤ 𝓜 μ (f + g)ψ:↥(SpaceDHilbertSpace d μ)hψ:ψ ∈ (𝓜 μ (f + g)).domainx:Space dh:‖g x‖ ≤ c' * ‖f x + g x‖⊢ c' * (‖f x + g x‖ * ‖↑↑ψ x‖) ≤ ‖(↑c' • (f + g) • ↑↑ψ) x‖ d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂhf:AEStronglyMeasurable f μhg:AEStronglyMeasurable g μc:ℝc':ℝhf':∀ᵐ (x : Space d) ∂μ, ‖f x‖ ≤ c * ‖f x + g x‖hg':∀ᵐ (x : Space d) ∂μ, ‖g x‖ ≤ c' * ‖f x + g x‖hle:𝓜 μ f + 𝓜 μ g ≤ 𝓜 μ (f + g)ψ:↥(SpaceDHilbertSpace d μ)hψ:ψ ∈ (𝓜 μ (f + g)).domainx:Space dh:‖g x‖ ≤ c' * ‖f x + g x‖⊢ ‖(g • ↑↑ψ) x‖ ≤ c' * (‖f x + g x‖ * ‖↑↑ψ x‖) All goals completed! 🐙 d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂhf:AEStronglyMeasurable f μhg:AEStronglyMeasurable g μc:ℝc':ℝhf':∀ᵐ (x : Space d) ∂μ, ‖f x‖ ≤ c * ‖f x + g x‖hg':∀ᵐ (x : Space d) ∂μ, ‖g x‖ ≤ c' * ‖f x + g x‖hle:𝓜 μ f + 𝓜 μ g ≤ 𝓜 μ (f + g)ψ:↥(SpaceDHilbertSpace d μ)hψ:ψ ∈ (𝓜 μ (f + g)).domainx:Space dh:‖g x‖ ≤ c' * ‖f x + g x‖⊢ c' * (‖f x + g x‖ * ‖↑↑ψ x‖) ≤ ‖(↑c' • (f + g) • ↑↑ψ) x‖ exact le_of_le_of_eq (mul_le_mul_of_nonneg_right (le_abs_self c') (d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂhf:AEStronglyMeasurable f μhg:AEStronglyMeasurable g μc:ℝc':ℝhf':∀ᵐ (x : Space d) ∂μ, ‖f x‖ ≤ c * ‖f x + g x‖hg':∀ᵐ (x : Space d) ∂μ, ‖g x‖ ≤ c' * ‖f x + g x‖hle:𝓜 μ f + 𝓜 μ g ≤ 𝓜 μ (f + g)ψ:↥(SpaceDHilbertSpace d μ)hψ:ψ ∈ (𝓜 μ (f + g)).domainx:Space dh:‖g x‖ ≤ c' * ‖f x + g x‖⊢ 0 ≤ ‖f x + g x‖ * ‖↑↑ψ x‖ All goals completed! 🐙)) (d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂhf:AEStronglyMeasurable f μhg:AEStronglyMeasurable g μc:ℝc':ℝhf':∀ᵐ (x : Space d) ∂μ, ‖f x‖ ≤ c * ‖f x + g x‖hg':∀ᵐ (x : Space d) ∂μ, ‖g x‖ ≤ c' * ‖f x + g x‖hle:𝓜 μ f + 𝓜 μ g ≤ 𝓜 μ (f + g)ψ:↥(SpaceDHilbertSpace d μ)hψ:ψ ∈ (𝓜 μ (f + g)).domainx:Space dh:‖g x‖ ≤ c' * ‖f x + g x‖⊢ |c'| * (‖f x + g x‖ * ‖↑↑ψ x‖) = ‖(↑c' • (f + g) • ↑↑ψ) x‖ All goals completed! 🐙)

𝓜 μ (f - g) extends 𝓜 μ f - 𝓜 μ g.

In general the domains do not match: ψ ∈ (𝓜 μ f - 𝓜 μ g).domain amounts to MemHS (f • ψ) μ and MemHS (g • ψ) μ whereas ψ ∈ (𝓜 μ (f - g)).domain is equivalent to the weaker condition MemHS ((f - g) • ψ) μ.

See mulOperator_sub_eq and mulOperator_sub_eq' for sufficient conditions to ensure equality.

lemma mulOperator_sub_ge (μ : Measure (Space d)) (f g : Space d → ℂ) : 𝓜 μ f - 𝓜 μ g ≤ 𝓜 μ (f - g) := le_of_eq_of_le (d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂ⊢ 𝓜 μ f - 𝓜 μ g = 𝓜 μ f + 𝓜 μ (-g) All goals completed! 🐙) (mulOperator_add_ge μ f (-g))

(𝓜 μ g).domain = ⊤ is a sufficient condition to ensure equality in mulOperator_sub_ge.

@[simp] lemma mulOperator_sub_eq {μ : Measure (Space d)} (f : Space d → ℂ) {g : Space d → ℂ} (h : (𝓜 μ g).domain = ⊤) : 𝓜 μ (f - g) = 𝓜 μ f - 𝓜 μ g := d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂh:(𝓜 μ g).domain = ⊤⊢ 𝓜 μ (f - g) = 𝓜 μ f - 𝓜 μ g All goals completed! 🐙

Having both ‖f x‖ ≤ c * ‖f x - g x‖ and ‖g x‖ ≤ c' * ‖f x - g x‖ μ-a.e. is a sufficient condition to ensure equality in mulOperator_sub_ge.

lemma mulOperator_sub_eq' {μ : Measure (Space d)} {f g : Space d → ℂ} (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) (c c' : ℝ) (hf' : ∀ᵐ x ∂μ, ‖f x‖ ≤ c * ‖f x - g x‖) (hg' : ∀ᵐ x ∂μ, ‖g x‖ ≤ c' * ‖f x - g x‖) : 𝓜 μ (f - g) = 𝓜 μ f - 𝓜 μ g := d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂhf:AEStronglyMeasurable f μhg:AEStronglyMeasurable g μc:ℝc':ℝhf':∀ᵐ (x : Space d) ∂μ, ‖f x‖ ≤ c * ‖f x - g x‖hg':∀ᵐ (x : Space d) ∂μ, ‖g x‖ ≤ c' * ‖f x - g x‖⊢ 𝓜 μ (f - g) = 𝓜 μ f - 𝓜 μ g d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂhf:AEStronglyMeasurable f μhg:AEStronglyMeasurable g μc:ℝc':ℝhf':∀ᵐ (x : Space d) ∂μ, ‖f x‖ ≤ c * ‖f x - g x‖hg':∀ᵐ (x : Space d) ∂μ, ‖g x‖ ≤ c' * ‖f x - g x‖⊢ 𝓜 μ (f + -g) = 𝓜 μ f + 𝓜 μ (-g) exact mulOperator_add_eq' hf hg.neg c c' (d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂhf:AEStronglyMeasurable f μhg:AEStronglyMeasurable g μc:ℝc':ℝhf':∀ᵐ (x : Space d) ∂μ, ‖f x‖ ≤ c * ‖f x - g x‖hg':∀ᵐ (x : Space d) ∂μ, ‖g x‖ ≤ c' * ‖f x - g x‖⊢ ∀ᵐ (x : Space d) ∂μ, ‖f x‖ ≤ c * ‖f x + (-g) x‖ All goals completed! 🐙) (d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂhf:AEStronglyMeasurable f μhg:AEStronglyMeasurable g μc:ℝc':ℝhf':∀ᵐ (x : Space d) ∂μ, ‖f x‖ ≤ c * ‖f x - g x‖hg':∀ᵐ (x : Space d) ∂μ, ‖g x‖ ≤ c' * ‖f x - g x‖⊢ ∀ᵐ (x : Space d) ∂μ, ‖(-g) x‖ ≤ c' * ‖f x + (-g) x‖ All goals completed! 🐙)
TODO "Add to the sufficient conditions which ensure `𝓜 μ (f ± g) = 𝓜 μ f ± 𝓜 μ g`."

E.3. Composition

𝓜 μ (f • g) extends 𝓜 μ f * 𝓜 μ g.

In general the domains do not match: ψ ∈ (𝓜 μ f * 𝓜 μ g).domain amounts to MemHS (g • ψ) μ and MemHS (f • g • ψ) μ whereas ψ ∈ (𝓜 μ (f • g)).domain only requires MemHS (f • g • ψ) μ.

See mulOperator_smul_eq for a sufficient condition to ensure equality.

lemma mulOperator_smul_ge (μ : Measure (Space d)) (f g : Space d → ℂ) : 𝓜 μ f ∘ᵣ 𝓜 μ g ≤ 𝓜 μ (f • g) := d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂ⊢ 𝓜 μ f ∘ᵣ 𝓜 μ g ≤ 𝓜 μ (f • g) d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂ⊢ (𝓜 μ f ∘ᵣ 𝓜 μ g).domain ≤ (𝓜 μ (f • g)).domaind:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂ⊢ ∀ ⦃x : ↥(𝓜 μ f ∘ᵣ 𝓜 μ g).domain⦄ ⦃y : ↥(𝓜 μ (f • g)).domain⦄, ↑x = ↑y → ↑(𝓜 μ f ∘ᵣ 𝓜 μ g) x = ↑(𝓜 μ (f • g)) y d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂ⊢ (𝓜 μ f ∘ᵣ 𝓜 μ g).domain ≤ (𝓜 μ (f • g)).domain d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂψ:↥(SpaceDHilbertSpace d μ)hψ:ψ ∈ (𝓜 μ f ∘ᵣ 𝓜 μ g).domain⊢ ψ ∈ (𝓜 μ (f • g)).domain d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂψ:↥(SpaceDHilbertSpace d μ)hψ✝:ψ ∈ (𝓜 μ f ∘ᵣ 𝓜 μ g).domainhψ:ψ ∈ (𝓜 μ g).domainhgψ:↑(𝓜 μ g) ⟨ψ, hψ⟩ ∈ (𝓜 μ f).domain⊢ ψ ∈ (𝓜 μ (f • g)).domain d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂψ:↥(SpaceDHilbertSpace d μ)hψ✝:ψ ∈ (𝓜 μ f ∘ᵣ 𝓜 μ g).domainhψ:ψ ∈ (𝓜 μ g).domainhgψ:↑(𝓜 μ g) ⟨ψ, hψ⟩ ∈ (𝓜 μ f).domain⊢ f • ↑↑(↑(𝓜 μ g) ⟨ψ, hψ⟩) =ᵐ[μ] (f • g) • ↑↑ψ d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂψ:↥(SpaceDHilbertSpace d μ)hψ✝:ψ ∈ (𝓜 μ f ∘ᵣ 𝓜 μ g).domainhψ:ψ ∈ (𝓜 μ g).domainhgψ:↑(𝓜 μ g) ⟨ψ, hψ⟩ ∈ (𝓜 μ f).domain⊢ ∀ (a : Space d), ↑↑(↑(𝓜 μ g) ⟨ψ, hψ⟩) a = (g • ↑↑ψ) a → (f • ↑↑(↑(𝓜 μ g) ⟨ψ, hψ⟩)) a = ((f • g) • ↑↑ψ) a All goals completed! 🐙 d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂ⊢ ∀ ⦃x : ↥(𝓜 μ f ∘ᵣ 𝓜 μ g).domain⦄ ⦃y : ↥(𝓜 μ (f • g)).domain⦄, ↑x = ↑y → ↑(𝓜 μ f ∘ᵣ 𝓜 μ g) x = ↑(𝓜 μ (f • g)) y d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂψ:↥(𝓜 μ f ∘ᵣ 𝓜 μ g).domainφ:↥(𝓜 μ (f • g)).domainhψφ:↑ψ = ↑φ⊢ ↑(𝓜 μ f ∘ᵣ 𝓜 μ g) ψ = ↑(𝓜 μ (f • g)) φ d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂψ:↥(𝓜 μ f ∘ᵣ 𝓜 μ g).domainφ:↥(𝓜 μ (f • g)).domainhψφ:↑ψ = ↑φ⊢ ↑↑(↑(𝓜 μ f ∘ᵣ 𝓜 μ g) ψ) =ᵐ[μ] ↑↑(↑(𝓜 μ (f • g)) φ) d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂψ:↥(𝓜 μ f ∘ᵣ 𝓜 μ g).domainφ:↥(𝓜 μ (f • g)).domainhψφ:↑ψ = ↑φhψ:↑ψ ∈ (𝓜 μ g).domainhgψ:↑(𝓜 μ g) ⟨↑ψ, hψ⟩ ∈ (𝓜 μ f).domain⊢ ↑↑(↑(𝓜 μ f ∘ᵣ 𝓜 μ g) ψ) =ᵐ[μ] ↑↑(↑(𝓜 μ (f • g)) φ) d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂψ:↥(𝓜 μ f ∘ᵣ 𝓜 μ g).domainφ:↥(𝓜 μ (f • g)).domainhψφ:↑ψ = ↑φhψ:↑ψ ∈ (𝓜 μ g).domainhgψ:↑(𝓜 μ g) ⟨↑ψ, hψ⟩ ∈ (𝓜 μ f).domain⊢ ∀ (a : Space d), ↑↑(↑(𝓜 μ (f • g)) φ) a = ((f • g) • ↑↑↑φ) a → ↑↑(↑(𝓜 μ g) ⟨↑ψ, hψ⟩) a = (g • ↑↑↑ψ) a → ↑↑(↑(𝓜 μ f) ⟨↑(𝓜 μ g) ⟨↑ψ, hψ⟩, hgψ⟩) a = (f • ↑↑(↑(𝓜 μ g) ⟨↑ψ, hψ⟩)) a → ↑↑(↑(𝓜 μ f ∘ᵣ 𝓜 μ g) ψ) a = ↑↑(↑(𝓜 μ (f • g)) φ) a All goals completed! 🐙

(𝓜 μ g).domain = ⊤ is a sufficient condition to ensure equality in mulOperator_smul_ge.

lemma mulOperator_smul_eq {μ : Measure (Space d)} (f : Space d → ℂ) {g : Space d → ℂ} (h : (𝓜 μ g).domain = ⊤) : 𝓜 μ f ∘ᵣ 𝓜 μ g = 𝓜 μ (f • g) := d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂh:(𝓜 μ g).domain = ⊤⊢ 𝓜 μ f ∘ᵣ 𝓜 μ g = 𝓜 μ (f • g) d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂh:(𝓜 μ g).domain = ⊤hle:𝓜 μ f ∘ᵣ 𝓜 μ g ≤ 𝓜 μ (f • g)⊢ 𝓜 μ f ∘ᵣ 𝓜 μ g = 𝓜 μ (f • g) d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂh:(𝓜 μ g).domain = ⊤hle:𝓜 μ f ∘ᵣ 𝓜 μ g ≤ 𝓜 μ (f • g)⊢ (𝓜 μ f ∘ᵣ 𝓜 μ g).domain = (𝓜 μ (f • g)).domain d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂh:(𝓜 μ g).domain = ⊤hle:𝓜 μ f ∘ᵣ 𝓜 μ g ≤ 𝓜 μ (f • g)ψ:↥(SpaceDHilbertSpace d μ)hψ:ψ ∈ (𝓜 μ (f • g)).domain⊢ ψ ∈ (𝓜 μ f ∘ᵣ 𝓜 μ g).domain d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂh:(𝓜 μ g).domain = ⊤hle:𝓜 μ f ∘ᵣ 𝓜 μ g ≤ 𝓜 μ (f • g)ψ:↥(SpaceDHilbertSpace d μ)hψ:ψ ∈ (𝓜 μ (f • g)).domain⊢ ↑(𝓜 μ g) ⟨ψ, ⋯⟩ ∈ (𝓜 μ f).domain d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂh:(𝓜 μ g).domain = ⊤hle:𝓜 μ f ∘ᵣ 𝓜 μ g ≤ 𝓜 μ (f • g)ψ:↥(SpaceDHilbertSpace d μ)hψ:ψ ∈ (𝓜 μ (f • g)).domain⊢ (f • g) • ↑↑ψ =ᵐ[μ] f • ↑↑(↑(𝓜 μ g) ⟨ψ, ⋯⟩) d:ℕμ:Measure (Space d)f:Space d → ℂg:Space d → ℂh:(𝓜 μ g).domain = ⊤hle:𝓜 μ f ∘ᵣ 𝓜 μ g ≤ 𝓜 μ (f • g)ψ:↥(SpaceDHilbertSpace d μ)hψ:ψ ∈ (𝓜 μ (f • g)).domain⊢ ∀ (a : Space d), ↑↑(↑(𝓜 μ g) ⟨ψ, ⋯⟩) a = (g • ↑↑ψ) a → ((f • g) • ↑↑ψ) a = (f • ↑↑(↑(𝓜 μ g) ⟨ψ, ⋯⟩)) a All goals completed! 🐙
TODO "`mulOperator_smul_eq` has the strong assumption `(𝓜 μ g).domain = ⊤`. Weaken this assumption and/or find other sufficient conditions to ensure the equality `𝓜 μ (f • g) = 𝓜 μ f * 𝓜 μ g`."

F. Spectrum

TODO "Prove that the spectrum of the multiplication operator `𝓜 μ f` is the 'μ-essential range' of `f`."TODO "Prove that the spectrum of the multiplication operator `𝓜 μ f` is the closure of `f.range` for continuous `f`."