Physicslib4.Spectral.Stone.Bounded

The unitary group of a bounded self-adjoint operator

For a bounded operator P, t ↦ exp(itP) (the norm-convergent exponential series) is differentiable at 0 with derivative iP; for self-adjoint P it is a one-parameter unitary group, strongly continuous, with generator P on all of H (blueprint §10.4.1).

theorem Physicslib4.Spectral.Stone.hasDerivAt_exp_smul_I {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (P : H →L[ℂ] H) : HasDerivAt (fun (t : ℝ) => NormedSpace.exp ((↑t * Complex.I) • P)) (Complex.I • P) 0

t ↦ exp(itP) is differentiable at 0 in the operator norm, with derivative iP.

Blueprint reference: lmm:exp-bounded-hasDerivAt.

theorem Physicslib4.Spectral.Stone.exists_isOneParameterUnitaryGroup_exp {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {P : H →L[ℂ] H} (hP : IsSelfAdjoint P) : ∃ (V : ℝ → H ≃ₗᵢ[ℂ] H), (∀ (t : ℝ) (x : H), (V t) x = (NormedSpace.exp ((↑t * Complex.I) • P)) x) ∧ IsOneParameterUnitaryGroup V

For a bounded self-adjoint operator P, the exponentials exp(itP), t ∈ ℝ, form a one-parameter unitary group.

Here exp(itP) is the power series Σ (itP)ⁿ/n!, which converges in operator norm because P is bounded. Self-adjointness makes itP skew-adjoint, (itP)* = −itP, so each exp(itP) is unitary; and itP commutes with isP, so exp(i(s + t)P) = exp(isP) exp(itP). This case of Stone's theorem needs no spectral theory. A Hamiltonian on a finite-dimensional space, such as that of a spin in a magnetic field, is of this kind.

Implementation note: the exponential is Mathlib's NormedSpace.exp applied to (t i) • P. The statement produces a family V : ℝ → (H ≃ₗᵢ[ℂ] H) agreeing with it pointwise; the proof shows that exp(itP) lies in Mathlib's unitary (H →L[ℂ] H) and converts it with Unitary.linearIsometryEquiv.

Blueprint: lmm:exp-bounded-unitary-group

theorem Physicslib4.Spectral.Stone.isStronglyContinuous_of_eq_exp {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {P : H →L[ℂ] H} {V : ℝ → H ≃ₗᵢ[ℂ] H} (hV : ∀ (t : ℝ) (x : H), (V t) x = (NormedSpace.exp ((↑t * Complex.I) • P)) x) : IsStronglyContinuous V

A unitary family V with V t = exp(itP) is strongly continuous. The blueprint takes P self-adjoint, which is what makes exp(itP) unitary; here unitarity is carried by the type of V, so no hypothesis on P is needed.

Blueprint reference: lmm:generator-exp-bounded.

theorem Physicslib4.Spectral.Stone.generator_eq_of_eq_exp {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {P : H →L[ℂ] H} {V : ℝ → H ≃ₗᵢ[ℂ] H} (hV : ∀ (t : ℝ) (x : H), (V t) x = (NormedSpace.exp ((↑t * Complex.I) • P)) x) : generator V = (↑P).toPMap ⊤

If a unitary family V(t) equals exp(itP) for a bounded operator P, its infinitesimal generator is P, defined on all of H.

The map t ↦ exp(itP) is differentiable in operator norm with derivative iP at t = 0 (hasDerivAt_exp_smul_I), so the difference quotient (1/i)(V(t)ψ − ψ)/t tends to Pψ for every ψ. A bounded self-adjoint operator therefore generates exp(itP), as Stone's theorem predicts. Together with isStronglyContinuous_of_eq_exp this is the bounded case of the correspondence between self-adjoint operators and strongly continuous one-parameter unitary groups.

Implementation note: the blueprint takes P self-adjoint, which is what makes exp(itP) unitary. Here unitarity is carried by the type of V, so no hypothesis on P is needed. The conclusion is an equality of LinearPMaps with the operator P on the domain ⊤ = H.

Blueprint: lmm:generator-exp-bounded