Self-adjointness of the Stone generator

This file shows the infinitesimal generator of a strongly continuous one-parameter unitary group is self-adjoint, via the group's unitarity and the fundamental theorem of calculus for the difference quotient.

theorem StrongContUnitary.generator_domain_invariant {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (U : StrongContUnitary E) (s : ℝ) (x : ↥U.generator.domain) : (U.toFun s) ↑x ∈ U.generator.domain

The generator domain is invariant under its unitary group.

theorem StrongContUnitary.orbit_hasDerivAt {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (U : StrongContUnitary E) (x : ↥U.generator.domain) (s : ℝ) : HasDerivAt (fun (t : ℝ) => (U.toFun t) ↑x) (Complex.I • (U.toFun s) (↑U.generator x)) s

The derivative of a unitary orbit is given by its generator.

theorem StrongContUnitary.generator_isSelfAdjoint {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (U : StrongContUnitary E) : IsSelfAdjoint U.generator