Physlib.QuantumMechanics.DDimensions.Operators.SpectralTheory.SpectralMeasure

Spectral measures

i. Overview

A spectral measure `μS` on a measurable space `α` is a σ-additive function `Set α → H →L[ℂ] H` such that each set is mapped to a star projection on `H`, the empty set and non-measurable sets are mapped to zero, and `univ` is mapped to the identity. This is implemented as a structure extending `VectorMeasure α (H →L[ℂ] H)` with additional fields constraining `μS A` to be a star projection for each set `A` and `μS univ = 1`.

For each `x : H` there is an associated measure `μₓ` given by `μₓ A = ‖μS A x‖² = ⟪x, μS A x⟫ ≤ 1`.

ii. Key results

- `SpectralMeasure` : A star projection-valued measure. - `comp_eq_of_inter` : For a spectral measure `μS` and measurable sets `A` and `B`, the composition `μS A ∘ μS B = μS (A ∩ B)`.

iii. Table of contents

A. Definition
B. Composition

iv. References

A. Definition

B. Composition

9 declarations

instance

$\mathcal{L}(H)$ is torsion-free for complex inner product spaces $H$

#instIsAddTorsionFreeContinuousLinearMapComplexId_physlib

Let $H$ be a complex inner product space. The additive group of continuous $\mathbb{C}$ -linear maps from $H$ to itself, denoted by $\mathcal{L}(H)$ , is torsion-free. That is, for any operator $T \in \mathcal{L}(H)$ and any positive integer $n$ , if $n \cdot T = 0$ , then $T = 0$ .

instance

Coercion of a spectral measure to a vector measure on $\mathcal{L}(H)$

#instCoeVectorMeasure

Let $\alpha$ be a measurable space and $H$ be a complex inner product space. A spectral measure $\mu_S$ on $\alpha$ is coerced into a vector measure on $\alpha$ taking values in the space of continuous $\mathbb{C}$ -linear maps $\mathcal{L}(H)$ .

instance

Coercion of a spectral measure to a function $\text{Set } \alpha \to \mathcal{L}(H)$

#instCoeFun

Let $\alpha$ be a measurable space and $H$ be a complex inner product space. A spectral measure $\mu_S$ on $\alpha$ is treated as a function that maps a subset $A \subseteq \alpha$ to its corresponding continuous $\mathbb{C}$ -linear operator $\mu_S(A) \in \mathcal{L}(H)$ .

theorem

$\mu_S(A)$ is a star projection

#isStarProjection

Let $\alpha$ be a measurable space and $H$ be a complex inner product space. For any subset $A \subseteq \alpha$ , the operator $\mu_S(A)$ associated with a spectral measure $\mu_S$ is a star projection (a self-adjoint projection operator).

theorem

$\mu_S(\text{univ}) = I$

#univ

Let $\alpha$ be a measurable space and $H$ be a complex inner product space. For any spectral measure $\mu_S$ on $\alpha$ , the value of the measure at the universal set (the entire space $\alpha$ ) is the identity operator $I$ on $H$ , written as $\mu_S(\text{univ}) = I$ .

theorem

$\mu_S(A) \circ \mu_S(A) = \mu_S(A)$

#comp_self

Let $\mu_S$ be a spectral measure on a measurable space $\alpha$ . For any set $A \subseteq \alpha$ , the composition of the bounded linear operator $\mu_S(A)$ with itself is equal to $\mu_S(A)$ , that is, $\mu_S(A) \circ \mu_S(A) = \mu_S(A)$ .

theorem

$\mu_S(A) \circ \mu_S(B) = 0$ for Disjoint Measurable Sets $A, B$

#comp_of_disjoint

Let $\mu_S$ be a spectral measure on a measurable space $\alpha$ . For any two disjoint measurable sets $A, B \subseteq \alpha$ , the composition of the bounded linear operators $\mu_S(A)$ and $\mu_S(B)$ is equal to the zero operator, denoted by $\mu_S(A) \circ \mu_S(B) = 0$ .

theorem

$\mu_S(A) \circ \mu_S(B) = \mu_S(A \cap B)$ for Measurable Sets $A, B$

#comp_eq_of_inter

Let $\mu_S$ be a spectral measure on a measurable space $\alpha$ . For any measurable sets $A, B \subseteq \alpha$ , the composition of the bounded linear operators $\mu_S(A)$ and $\mu_S(B)$ is equal to the operator associated with their intersection, given by $\mu_S(A) \circ \mu_S(B) = \mu_S(A \cap B)$ .

theorem

$\mu_S(A)$ and $\mu_S(B)$ commute for all $A, B$

#commute

Let $\mu_S$ be a spectral measure on a measurable space $\alpha$ . For any two sets $A, B \subseteq \alpha$ , the bounded linear operators $\mu_S(A)$ and $\mu_S(B)$ commute, such that $\mu_S(A) \circ \mu_S(B) = \mu_S(B) \circ \mu_S(A)$ .

Physlib.QuantumMechanics.DDimensions.Operators.SpectralTheory.SpectralMeasure

Spectral measures

i. Overview

ii. Key results

iii. Table of contents

iv. References

A. Definition

B. Composition

L(H)\mathcal{L}(H)L(H) is torsion-free for complex inner product spaces HHH

Coercion of a spectral measure to a vector measure on L(H)\mathcal{L}(H)L(H)

Coercion of a spectral measure to a function Set α→L(H)\text{Set } \alpha \to \mathcal{L}(H)Set α→L(H)

μS(A)\mu_S(A)μS​(A) is a star projection

μS(univ)=I\mu_S(\text{univ}) = IμS​(univ)=I

μS(A)∘μS(A)=μS(A)\mu_S(A) \circ \mu_S(A) = \mu_S(A)μS​(A)∘μS​(A)=μS​(A)

μS(A)∘μS(B)=0\mu_S(A) \circ \mu_S(B) = 0μS​(A)∘μS​(B)=0 for Disjoint Measurable Sets A,BA, BA,B

μS(A)∘μS(B)=μS(A∩B)\mu_S(A) \circ \mu_S(B) = \mu_S(A \cap B)μS​(A)∘μS​(B)=μS​(A∩B) for Measurable Sets A,BA, BA,B

μS(A)\mu_S(A)μS​(A) and μS(B)\mu_S(B)μS​(B) commute for all A,BA, BA,B

$\mathcal{L}(H)$ is torsion-free for complex inner product spaces $H$

Coercion of a spectral measure to a vector measure on $\mathcal{L}(H)$

Coercion of a spectral measure to a function $\text{Set } \alpha \to \mathcal{L}(H)$

$\mu_S(A)$ is a star projection

$\mu_S(\text{univ}) = I$

$\mu_S(A) \circ \mu_S(A) = \mu_S(A)$

$\mu_S(A) \circ \mu_S(B) = 0$ for Disjoint Measurable Sets $A, B$

$\mu_S(A) \circ \mu_S(B) = \mu_S(A \cap B)$ for Measurable Sets $A, B$

$\mu_S(A)$ and $\mu_S(B)$ commute for all $A, B$