Stone's theorem: unitary groups from self-adjoint generators

This file constructs a strongly continuous unitary group from a self-adjoint operator's spectral functional calculus applied to the phase function t ↦ exp(i t r), and shows it generates the original operator, completing Stone's theorem in the direction from self-adjoint operators to unitary groups.

noncomputable def stonePhase (t r : ℝ) : ℂ

The complex unit phase at time t and spectral coordinate r.

Equations

• stonePhase t r = Complex.exp (Complex.I * ↑t * ↑r)

theorem stonePhase_measurable (t : ℝ) : Measurable (stonePhase t)

theorem stonePhase_norm (t r : ℝ) : ‖stonePhase t r‖ = 1

theorem stonePhase_bounded (t r : ℝ) : ‖stonePhase t r‖ ≤ 1

noncomputable def spectralEvolution {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) (t : ℝ) : E →L[ℂ] E

The bounded evolution operator obtained by integrating the unit phase against a PVM.

Equations

• spectralEvolution E_pvm t = E_pvm.integral (stonePhase t) ⋯ ⋯

noncomputable def spectralUnitaryGroup {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) : StrongContUnitary E

The strongly continuous unitary group assembled from spectral evolution operators.

Equations

• spectralUnitaryGroup E_pvm = { toFun := spectralEvolution E_pvm, isUnitary := ⋯, zero := ⋯, add := ⋯, stronglyContinuous := ⋯ }

noncomputable def PVM.phaseUnitaryGroup {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) : StrongContUnitary E

The unitary group obtained by integrating the phases exp (i t r) against a PVM.

Equations

• E_pvm.phaseUnitaryGroup = spectralUnitaryGroup E_pvm

theorem PVM.phaseUnitaryGroup_generator {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (E_pvm : PVM E) : E_pvm.phaseUnitaryGroup.generator = E_pvm.unboundedIntegral Complex.ofReal ⋯

The generator of the phase unitary group is integration against the real coordinate.

noncomputable def selfAdjointGeneratesUnitaryGroup {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →ₗ.[ℂ] E) (hA : IsSelfAdjoint A) : StrongContUnitary E

A self-adjoint operator generates a strongly continuous one-parameter unitary group.

Equations

• selfAdjointGeneratesUnitaryGroup A hA = (Classical.choose ⋯).phaseUnitaryGroup

theorem selfAdjoint_generates_unitary_group_generator {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →ₗ.[ℂ] E) (hA : IsSelfAdjoint A) : (selfAdjointGeneratesUnitaryGroup A hA).generator = A

The phase unitary group constructed from a self-adjoint operator has generator A.