Stone's theorem for unbounded self-adjoint operators

A self-adjoint operator A on a complex Hilbert space is -i times the complex generator of exactly one unitary C₀-group, the group e^{itA}. This completes the converse direction of Stone's theorem, begun for bounded A in TauCeti.Analysis.Semigroups.Group.Stone.Basic. Together with the skew-adjointness of the generator of a unitary group (TauCeti.Semigroups.StronglyContinuousGroup.IsUnitary.complexGenerator_adjoint_eq_neg) this characterizes the self-adjoint operators as the operators A with i • A the complex generator of a unitary group.

The construction is the classical one. The real restrictions of i • A and -i • A are m-dissipative (IsSelfAdjoint.isMDissipative_smul_restrictScalars at c = ± i), so by Lumer--Phillips each generates a contraction semigroup. Their generators are negatives of one another, so their equal-time operators are mutually inverse and the two semigroups glue into a C₀-group (TauCeti.Semigroups.StronglyContinuousSemigroup.toGroupOfInverse, the inverse hypotheses being StronglyContinuousSemigroup.comp_eq_id_of_generator_eq_neg and its primed variant). The glued group is complex linear because its forward half is (the generator of that half is the real restriction of a complex-linear partial map), and unitary because it contracts in both time directions. Its complex generator is i • A, and a unitary group is determined by its complex generator.

Main results

• IsSelfAdjoint.existsUnique_isUnitary_complexGenerator_eq_I_smul: Stone's theorem, converse direction: a self-adjoint operator A has exactly one unitary C₀-group with complex generator i • A.
• LinearPMap.isSelfAdjoint_iff_exists_isUnitary_complexGenerator_eq_I_smul is Stone's theorem as a characterization of self-adjoint operators.

References

• K.-J. Engel and R. Nagel, One-Parameter Semigroups for Linear Evolution Equations, Theorem II.3.24.
• M. Reed and B. Simon, Methods of Modern Mathematical Physics I: Functional Analysis, Theorem VIII.7 and Theorem VIII.8.

theorem IsSelfAdjoint.exists_isUnitary_complexGenerator_eq_I_smul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →ₗ.[ℂ] H} (hA : IsSelfAdjoint A) : ∃ (U : TauCeti.Semigroups.StronglyContinuousGroup H) (hU : U.IsUnitary), U.complexGenerator hU = Complex.I • A

Stone's theorem, converse direction (existence). A self-adjoint operator A on a complex Hilbert space is -i times the complex generator of a unitary C₀-group.

theorem IsSelfAdjoint.existsUnique_isUnitary_complexGenerator_eq_I_smul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →ₗ.[ℂ] H} (hA : IsSelfAdjoint A) : ∃! U : TauCeti.Semigroups.StronglyContinuousGroup H, ∃ (hU : U.IsUnitary), U.complexGenerator hU = Complex.I • A

Stone's theorem, converse direction. A self-adjoint operator A on a complex Hilbert space is -i times the complex generator of exactly one unitary C₀-group.

theorem LinearPMap.isSelfAdjoint_iff_exists_isUnitary_complexGenerator_eq_I_smul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (A : H →ₗ.[ℂ] H) : IsSelfAdjoint A ↔ ∃ (U : TauCeti.Semigroups.StronglyContinuousGroup H) (hU : U.IsUnitary), U.complexGenerator hU = Complex.I • A

Stone's theorem. An operator A on a complex Hilbert space is self-adjoint if and only if i • A is the complex generator of a unitary C₀-group.