Physicslib4.Spectral.Stone.Theorem

Stone's theorem

Every strongly continuous one-parameter unitary group U on a Hilbert space is e^{itA} for a unique self-adjoint operator A, its infinitesimal generator (blueprint §10.4.5, Theorem thrm:hall-10.15).

The generator is essentially self-adjoint (its deficiency subspaces are trivial, by an ODE argument along orbits); the orbits of U and of e^{itA^cl} agree on the generator's domain (their difference has constant norm); so U(t) = e^{itA^cl} by density, and the generator of e^{itA^cl} is A^cl (Proposition prpstn:hall-10.14), whence A = A^cl.

Main statements

• isEssentiallySelfAdjoint_generator — the generator is essentially self-adjoint.
• stone — Stone's theorem.

theorem Physicslib4.Spectral.Stone.hasDerivAt_inner_orbit {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {U : ℝ → H ≃ₗᵢ[ℂ] H} (hU : IsOneParameterUnitaryGroup U) (hc : IsStronglyContinuous U) (ε : ℂ) {ψ : H} (hψ : ψ ∈ (generator U).adjoint.domain) (hAψ : ↑(generator U).adjoint ⟨ψ, hψ⟩ = (ε * Complex.I) • ψ) (φ : ↥(generator U).domain) (t : ℝ) : HasDerivAt (fun (s : ℝ) => inner ℂ ((U s) ↑φ) ψ) (ε * inner ℂ ((U t) ↑φ) ψ) t

An ODE along orbits: if A* ψ = (ε i) ψ and φ ∈ Dom(A), then y(t) = ⟪U(t) φ, ψ⟫ satisfies y' = ε y. The blueprint takes ε = ±1; the computation holds for every ε ∈ ℂ.

Blueprint reference: lmm:orbit-inner-ode.

theorem Physicslib4.Spectral.Stone.eq_zero_of_hasDerivAt_of_bounded {y : ℝ → ℂ} {ε : ℝ} (hε : ε ≠ 0) (hy : ∀ (t : ℝ), HasDerivAt y (↑ε * y t) t) (hb : ∃ (C : ℝ), ∀ (t : ℝ), ‖y t‖ ≤ C) : y 0 = 0

Bounded solutions of y' = ε y vanish at 0. The blueprint takes ε = ±1; any nonzero real ε will do.

Blueprint reference: lmm:bounded-exp-solution-zero.

theorem Physicslib4.Spectral.Stone.ker_adjoint_generator_subSmul_eq_bot {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {U : ℝ → H ≃ₗᵢ[ℂ] H} (hU : IsOneParameterUnitaryGroup U) (hc : IsStronglyContinuous U) : Unbounded.ker (Unbounded.subSmul (generator U).adjoint Complex.I) = ⊥ ∧ Unbounded.ker (Unbounded.subSmul (generator U).adjoint (-Complex.I)) = ⊥

The deficiency subspaces of the generator are trivial: Ker(A* - i 1) = {0} and Ker(A* + i 1) = {0}.

Blueprint reference: lmm:generator-ker-adjoint-trivial.

theorem Physicslib4.Spectral.Stone.isEssentiallySelfAdjoint_generator {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {U : ℝ → H ≃ₗᵢ[ℂ] H} (hU : IsOneParameterUnitaryGroup U) (hc : IsStronglyContinuous U) : Unbounded.IsEssentiallySelfAdjoint (generator U)

The generator of a strongly continuous one-parameter unitary group is essentially self-adjoint: symmetric, closable, with self-adjoint closure. Its density is hasDenseDomain_generator.

Blueprint reference: lmm:generator-essentially-self-adjoint.

theorem Physicslib4.Spectral.Stone.hasDerivAt_orbit_sub_expUnitary {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {U : ℝ → H ≃ₗᵢ[ℂ] H} (hU : IsOneParameterUnitaryGroup U) (hc : IsStronglyContinuous U) (ψ : ↥(generator U).domain) (t : ℝ) : ∃ (h : (U t) ↑ψ - (expUnitary ⋯ t) ↑ψ ∈ (generator U).closure.domain), HasDerivAt (fun (s : ℝ) => (U s) ↑ψ - (expUnitary ⋯ s) ↑ψ) (Complex.I • ↑(generator U).closure ⟨(U t) ↑ψ - (expUnitary ⋯ t) ↑ψ, h⟩) t

The difference w(t) = U(t) ψ - e^{itA^cl} ψ of the orbits of ψ ∈ Dom(A) lies in Dom(A^cl) and has derivative i A^cl w(t).

Blueprint reference: lmm:orbit-difference-hasDerivAt.

theorem Physicslib4.Spectral.Stone.eq_zero_of_hasDerivAt_of_isSymmetric {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {C : H →ₗ.[ℂ] H} (hC : Unbounded.IsSymmetric C) {w : ℝ → H} (hw : ∀ (t : ℝ), ∃ (h : w t ∈ C.domain), HasDerivAt w (Complex.I • ↑C ⟨w t, h⟩) t) (h0 : w 0 = 0) (t : ℝ) : w t = 0

A solution of w' = i C w with C symmetric and w(0) = 0 vanishes identically, since ‖w(t)‖² is constant.

Blueprint reference: lmm:norm-const-of-symmetric-derivative.

theorem Physicslib4.Spectral.Stone.orbit_eq_expUnitary_closure {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {U : ℝ → H ≃ₗᵢ[ℂ] H} (hU : IsOneParameterUnitaryGroup U) (hc : IsStronglyContinuous U) (ψ : ↥(generator U).domain) (t : ℝ) : (U t) ↑ψ = (expUnitary ⋯ t) ↑ψ

The orbits of U and of e^{itA^cl} agree on the generator's domain.

Blueprint reference: lmm:orbits-agree-on-domain.

theorem Physicslib4.Spectral.Stone.eq_of_eqOn_dense {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {S T : H →L[ℂ] H} {D : Submodule ℂ H} (hD : Dense ↑D) (h : ∀ ψ ∈ D, S ψ = T ψ) : S = T

Bounded operators agreeing on a dense subspace are equal.

Blueprint reference: lmm:agree-on-dense-subspace.

theorem Physicslib4.Spectral.Stone.stone {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {U : ℝ → H ≃ₗᵢ[ℂ] H} (hU : IsOneParameterUnitaryGroup U) (hc : IsStronglyContinuous U) : ∃ (hA : IsSelfAdjoint (generator U)), Unbounded.HasDenseDomain (generator U) ∧ (∀ (t : ℝ), U t = expUnitary hA t) ∧ ∀ (B : H →ₗ.[ℂ] H) (hB : IsSelfAdjoint B), (∀ (t : ℝ), U t = expUnitary hB t) → B = generator U

Stone's theorem: the infinitesimal generator A of a strongly continuous one-parameter unitary group U is densely defined and self-adjoint, U(t) = e^(itA) for every t, and A is the only self-adjoint operator with this property.

Together with generator_expUnitary this gives a one-to-one correspondence between self-adjoint operators and strongly continuous one-parameter unitary groups: A ↦ e^(itA) one way, U ↦ its generator the other. It is why every continuous one-parameter symmetry of a quantum system comes with an observable: the Hamiltonian for time translations, momentum for spatial translations, angular momentum for rotations about an axis, up to sign and factors of ħ.

The proof has three steps. The generator is essentially self-adjoint: its deficiency subspaces Ker(A* ∓ i𝟙) are trivial, by an ODE argument along orbits (isEssentiallySelfAdjoint_generator). The orbits of U and of e^(itA^(cl)), for the closure A^(cl), agree on Dom(A), because their difference starts at 0 and has constant norm (orbit_eq_expUnitary_closure); so U(t) = e^(itA^(cl)), Dom(A) being dense. Finally the generator of e^(itA^(cl)) is A^(cl) (generator_expUnitary), so A = A^(cl) is self-adjoint.

Implementation note: expUnitary takes a proof of self-adjointness as an argument, so the statement opens with ∃ hA : IsSelfAdjoint (generator U) and writes e^(itA) as expUnitary hA t; U(t) = e^(itA) is an equality in H ≃ₗᵢ[ℂ] H. Uniqueness says that every self-adjoint B with U(t) = e^(itB) for all t equals the generator. The only assumption on H is completeness.

Blueprint: thrm:hall-10.15