The bounded part of Stone's theorem

This file begins the converse direction of Stone's theorem. A bounded self-adjoint operator A on a complex Hilbert space gives the unitary group exp (t i A); its real-linear generator is the expected operator i A. The general self-adjoint case is TauCeti.Analysis.Semigroups.Group.Stone.Unbounded.

noncomputable def TauCeti.Semigroups.StronglyContinuousGroup.ofBoundedExp {H : Type u_1} [NormedAddCommGroup H] [NormedSpace ℂ H] [CompleteSpace H] (A : H →L[ℂ] H) : StronglyContinuousGroup H

The exponential group associated to a bounded operator. It is unitary when the operator is self-adjoint.

Equations

• TauCeti.Semigroups.StronglyContinuousGroup.ofBoundedExp A = TauCeti.Semigroups.StronglyContinuousGroup.ofBounded (ContinuousLinearMap.restrictScalars ℝ (Complex.I • A))

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousGroup.ofBoundedExp_apply {H : Type u_1} [NormedAddCommGroup H] [NormedSpace ℂ H] [CompleteSpace H] (A : H →L[ℂ] H) (t : ℝ) : (ofBoundedExp A) t = ContinuousLinearMap.restrictScalars ℝ (NormedSpace.exp (↑t • Complex.I • A))

At time t, the bounded Stone group is the complex exponential regarded as real-linear.

@[simp]

theorem TauCeti.Semigroups.StronglyContinuousGroup.ofBoundedExp_generator {H : Type u_1} [NormedAddCommGroup H] [NormedSpace ℂ H] [CompleteSpace H] (A : H →L[ℂ] H) : (ofBoundedExp A).generator = (↑(ContinuousLinearMap.restrictScalars ℝ (Complex.I • A))).toPMap ⊤

The generator of the bounded exponential group is i A, regarded as a real partial linear map.

theorem TauCeti.Semigroups.StronglyContinuousGroup.isUnitary_ofBoundedExp {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (A : H →L[ℂ] H) (hA : IsSelfAdjoint A) : (ofBoundedExp A).IsUnitary

The bounded exponential group is unitary when its operator is self-adjoint.