Physicslib4.Spectral.Stone.Basic

One-parameter unitary groups and their infinitesimal generators

This file sets up the objects of Stone's theorem (blueprint §10.4).

Main definitions

• IsOneParameterUnitaryGroup U — U : ℝ → (H ≃ₗᵢ[ℂ] H) satisfies U 0 = 1 and U (s + t) = U s U t.
• IsStronglyContinuous U — every orbit t ↦ U t ψ is continuous.
• generatorQuotient U ψ t — the difference quotient (1/i) (U t ψ - ψ)/t.
• generator U — the infinitesimal generator, an unbounded operator whose domain is the set of ψ for which the punctured limit of generatorQuotient U ψ t as t → 0 exists, and whose value is that limit.

The generator is defined for any family U; the group law is assumed only in the results that need it.

structure Physicslib4.Spectral.Stone.IsOneParameterUnitaryGroup {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (U : ℝ → H ≃ₗᵢ[ℂ] H) : Prop

A family U(t), t ∈ ℝ, of unitary operators on H is a one-parameter unitary group: U(0) = 𝟙 and U(s + t) = U(s)U(t) for all real s and t.

Symmetries of a quantum system that depend on one real parameter, such as time translations, translations along a fixed direction or rotations about a fixed axis, act on the Hilbert space by unitary operators, and performing two of them in succession adds the parameters. The group law forces U(t)* = U(t)⁻¹ = U(−t) (IsOneParameterUnitaryGroup.adjoint_eq). No continuity in t is assumed; that is IsStronglyContinuous, and Stone's theorem (stone) uses both.

Implementation note: a unitary is a linear isometry equivalence H ≃ₗᵢ[ℂ] H, as elsewhere in the project, so each U(t) is unitary by its type and the structure records only the two group identities, stated vector by vector.

Blueprint: def:hall-10.11

• map_zero (ψ : H) : (U 0) ψ = ψ

  U(0) is the identity: U(0)ψ = ψ for every ψ.

• map_add (s t : ℝ) (ψ : H) : (U (s + t)) ψ = (U s) ((U t) ψ)

  The group law U(s + t) = U(s)U(t), applied to each vector ψ.

def Physicslib4.Spectral.Stone.IsStronglyContinuous {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (U : ℝ → H ≃ₗᵢ[ℂ] H) : Prop

A family U(t) of unitary operators is strongly continuous: t ↦ U(t)ψ is continuous for every vector ψ.

Strong continuity asks that each state vector move continuously, ‖U(t)ψ − U(s)ψ‖ → 0 as s → t, and not that U(s) → U(t) in operator norm. The weaker notion is the one physics needs: the translations (U(t)ψ)(x) = ψ(x + t) on L²(ℝ) are strongly continuous but not norm continuous. For a one-parameter unitary group, continuity at t = 0 already suffices (isStronglyContinuous_iff_tendsto_zero).

Implementation note: the predicate applies to any family U : ℝ → (H ≃ₗᵢ[ℂ] H); the group law is the separate hypothesis IsOneParameterUnitaryGroup U. Continuity is Mathlib's Continuous, for the norm topology of H.

Blueprint: def:hall-10.11

Equations

• Physicslib4.Spectral.Stone.IsStronglyContinuous U = ∀ (ψ : H), Continuous fun (t : ℝ) => (U t) ψ

noncomputable def Physicslib4.Spectral.Stone.generatorQuotient {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (U : ℝ → H ≃ₗᵢ[ℂ] H) (ψ : H) (t : ℝ) : H

The difference quotient (1/i)(U(t)ψ − ψ)/t, whose limit as t → 0, t ≠ 0, defines the infinitesimal generator.

If U(t) = e^(itA), then formally (U(t)ψ − ψ)/t → iAψ as t → 0, and the factor 1/i recovers Aψ. That factor fixes the sign convention: e^(itA) has generator A.

Implementation note: the quotient is written (it)⁻¹ • (U(t)ψ − ψ). At t = 0 it is 0, by Lean's convention 0⁻¹ = 0; the generator uses only the punctured limit, so this value plays no role.

Blueprint: def:hall-10.13

Equations

• Physicslib4.Spectral.Stone.generatorQuotient U ψ t = (Complex.I * ↑t)⁻¹ • ((U t) ψ - ψ)

theorem Physicslib4.Spectral.Stone.generatorQuotient_add {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (U : ℝ → H ≃ₗᵢ[ℂ] H) (φ ψ : H) (t : ℝ) : generatorQuotient U (φ + ψ) t = generatorQuotient U φ t + generatorQuotient U ψ t

theorem Physicslib4.Spectral.Stone.generatorQuotient_smul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (U : ℝ → H ≃ₗᵢ[ℂ] H) (c : ℂ) (ψ : H) (t : ℝ) : generatorQuotient U (c • ψ) t = c • generatorQuotient U ψ t

def Physicslib4.Spectral.Stone.generatorDomain {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (U : ℝ → H ≃ₗᵢ[ℂ] H) : Submodule ℂ H

The domain of the infinitesimal generator: the vectors ψ for which the difference quotient (1/i)(U(t)ψ − ψ)/t has a limit as t → 0, t ≠ 0.

In other words, ψ is in the domain when its orbit t ↦ U(t)ψ has a derivative at t = 0 in the norm of H. This is a subspace, since the quotient is linear in ψ and limits are linear. In general it is not all of H: for the translations (U(t)ψ)(x) = ψ(x + t) on L²(ℝ) it consists of the ψ whose derivative ψ' is again square integrable. For a strongly continuous one-parameter unitary group it is dense (hasDenseDomain_generator).

Implementation note: the limit is taken along the punctured neighbourhood filter 𝓝[≠] 0, and the domain is a Submodule ℂ H.

Blueprint: def:hall-10.13

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Physicslib4.Spectral.Stone.generator {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (U : ℝ → H ≃ₗᵢ[ℂ] H) : H →ₗ.[ℂ] H

The infinitesimal generator A of a family U(t) of unitaries: Aψ is the limit of (1/i)(U(t)ψ − ψ)/t as t → 0, t ≠ 0, on the subspace of vectors ψ where that limit exists.

Formally U(t) = e^(itA), and A is −i times the derivative of U(t) at t = 0. Stone's theorem (stone) makes this exact: for a strongly continuous one-parameter unitary group, A is self-adjoint and U(t) = e^(itA). Conversely, for self-adjoint A the group e^(itA) has generator A (generator_expUnitary). This is how observables arise from symmetries: the generator of the translations (U(t)ψ)(x) = ψ(x + t) on L²(ℝ) is the momentum operator −i d/dx, and in this sign convention a time evolution e^(−itĤ) has generator −Ĥ. The definition itself assumes nothing about U: no group law, no continuity, and no density of the domain. Those enter only the results about A; density of the domain is hasDenseDomain_generator.

Implementation note: A is a LinearPMap (H →ₗ.[ℂ] H) with domain generatorDomain U, and its value is Mathlib's limUnder along the punctured filter 𝓝[≠] 0, which is the limit wherever one exists. Membership and value are handled together by exists_generator_eq_iff.

Blueprint: def:hall-10.13

Equations

• One or more equations did not get rendered due to their size.

theorem Physicslib4.Spectral.Stone.generator_domain {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (U : ℝ → H ≃ₗᵢ[ℂ] H) : (generator U).domain = generatorDomain U

theorem Physicslib4.Spectral.Stone.isStronglyContinuous_iff_tendsto_zero {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {U : ℝ → H ≃ₗᵢ[ℂ] H} (hU : IsOneParameterUnitaryGroup U) : IsStronglyContinuous U ↔ ∀ (ψ : H), Filter.Tendsto (fun (s : ℝ) => (U s) ψ) (nhds 0) (nhds ψ)

A one-parameter unitary group is strongly continuous as soon as it is strongly continuous at 0: U s ψ → ψ as s → 0, for every ψ.

Blueprint reference: lmm:strongly-continuous-iff-at-zero.

theorem Physicslib4.Spectral.Stone.IsOneParameterUnitaryGroup.inner_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {U : ℝ → H ≃ₗᵢ[ℂ] H} (hU : IsOneParameterUnitaryGroup U) (t : ℝ) (φ ψ : H) : inner ℂ φ ((U t) ψ) = inner ℂ ((U (-t)) φ) ψ

The group law forces U(t)* = U(-t), in inner-product form: ⟪φ, U t ψ⟫ = ⟪U (-t) φ, ψ⟫.

Blueprint reference: lmm:unitary-group-inner-adjoint.

theorem Physicslib4.Spectral.Stone.IsOneParameterUnitaryGroup.adjoint_eq {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {U : ℝ → H ≃ₗᵢ[ℂ] H} (hU : IsOneParameterUnitaryGroup U) (t : ℝ) : ContinuousLinearMap.adjoint (U t).toLinearIsometry.toContinuousLinearMap = (U (-t)).toLinearIsometry.toContinuousLinearMap

The adjoint of U t is U (-t).

Blueprint reference: lmm:unitary-group-inner-adjoint.

theorem Physicslib4.Spectral.Stone.exists_generator_eq_iff {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (U : ℝ → H ≃ₗᵢ[ℂ] H) (ψ χ : H) : (∃ (h : ψ ∈ (generator U).domain), ↑(generator U) ⟨ψ, h⟩ = χ) ↔ Filter.Tendsto (generatorQuotient U ψ) (nhdsWithin 0 {0}ᶜ) (nhds χ)

Characterization of the generator: ψ ∈ Dom(A) with A ψ = χ if and only if the difference quotient (1/i) (U t ψ - ψ)/t tends to χ as t → 0, t ≠ 0.

Blueprint reference: lmm:generator-spec.

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

The generator of a one-parameter unitary group satisfies the symmetry identity ⟪φ, A ψ⟫ = ⟪A φ, ψ⟫ on its domain, which is symmetry in the density-free sense of Unbounded.IsSymmetric.

Blueprint reference: lmm:generator-symmetry-identity.

theorem Physicslib4.Spectral.Stone.eq_mul_exp_of_hasDerivAt {y : ℝ → ℂ} {c : ℂ} (hy : ∀ (t : ℝ), HasDerivAt y (c * y t) t) (t : ℝ) : y t = y 0 * Complex.exp (c * ↑t)

The scalar equation y' = c y: a differentiable y : ℝ → ℂ with y' = c y is y t = y 0 * exp (c t).

Blueprint reference: lmm:linear-ode-scalar.

theorem Physicslib4.Spectral.Stone.IsOneParameterUnitaryGroup.hasDerivAt_orbit {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {U : ℝ → H ≃ₗᵢ[ℂ] H} (hU : IsOneParameterUnitaryGroup U) (ψ : ↥(generator U).domain) (t : ℝ) : HasDerivAt (fun (s : ℝ) => (U s) ↑ψ) (Complex.I • (U t) (↑(generator U) ψ)) t

Orbits through the generator's domain are differentiable: for ψ ∈ Dom(A), s ↦ U s ψ has derivative i U t (A ψ) at every t.

Blueprint reference: lmm:orbit-hasDerivAt.

theorem Physicslib4.Spectral.Stone.IsOneParameterUnitaryGroup.generator_apply_comm {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {U : ℝ → H ≃ₗᵢ[ℂ] H} (hU : IsOneParameterUnitaryGroup U) (ψ : ↥(generator U).domain) (t : ℝ) : ∃ (h : (U t) ↑ψ ∈ (generator U).domain), ↑(generator U) ⟨(U t) ↑ψ, h⟩ = (U t) (↑(generator U) ψ)

The group commutes with its generator: for ψ ∈ Dom(A), U t ψ ∈ Dom(A) and A (U t ψ) = U t (A ψ).

Blueprint reference: lmm:generator-commutes.

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

The group preserves the generator's domain and differentiates to it: for ψ ∈ Dom(A) and every t, U t ψ ∈ Dom(A) and s ↦ U s ψ has derivative i U t (A ψ) = i A (U t ψ) at t.

The blueprint assumes U strongly continuous; the proof does not use it, so the hypothesis is omitted.

Blueprint reference: lmm:hall-10.17.

theorem Physicslib4.Spectral.Stone.isOneParameterUnitaryGroup_refl {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] : IsOneParameterUnitaryGroup fun (x : ℝ) => LinearIsometryEquiv.refl ℂ H

The trivial family t ↦ 1 is a one-parameter unitary group.

Blueprint reference: lmm:generator-const.

theorem Physicslib4.Spectral.Stone.isStronglyContinuous_refl {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] : IsStronglyContinuous fun (x : ℝ) => LinearIsometryEquiv.refl ℂ H

The trivial family t ↦ 1 is strongly continuous.

Blueprint reference: lmm:generator-const.

theorem Physicslib4.Spectral.Stone.generator_refl {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] : (generator fun (x : ℝ) => LinearIsometryEquiv.refl ℂ H) = 0

The generator of the trivial group t ↦ 1 is 0, with domain H.

Blueprint reference: lmm:generator-const.

theorem Physicslib4.Spectral.Stone.IsOneParameterUnitaryGroup.conj {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {U : ℝ → H ≃ₗᵢ[ℂ] H} (hU : IsOneParameterUnitaryGroup U) (W : H ≃ₗᵢ[ℂ] H) : IsOneParameterUnitaryGroup fun (t : ℝ) => (W.symm.trans (U t)).trans W

Conjugating a one-parameter unitary group by a unitary W gives a one-parameter unitary group t ↦ W U(t) W⁻¹.

Blueprint reference: lmm:conj-unitary-group.

theorem Physicslib4.Spectral.Stone.IsStronglyContinuous.conj {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {U : ℝ → H ≃ₗᵢ[ℂ] H} (hU : IsStronglyContinuous U) (W : H ≃ₗᵢ[ℂ] H) : IsStronglyContinuous fun (t : ℝ) => (W.symm.trans (U t)).trans W

Conjugation by a unitary preserves strong continuity.

Blueprint reference: lmm:conj-unitary-group.

theorem Physicslib4.Spectral.Stone.mem_generator_conj_domain_iff {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (U : ℝ → H ≃ₗᵢ[ℂ] H) (W : H ≃ₗᵢ[ℂ] H) (ψ : H) : ψ ∈ (generator fun (t : ℝ) => (W.symm.trans (U t)).trans W).domain ↔ W.symm ψ ∈ (generator U).domain

The domain of the generator of t ↦ W U(t) W⁻¹ is W · Dom(A), A the generator of U. No group law is needed: the difference quotient at ψ is W applied to that of U at W⁻¹ ψ.

Blueprint reference: lmm:generator-conj.

theorem Physicslib4.Spectral.Stone.generator_conj_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] (U : ℝ → H ≃ₗᵢ[ℂ] H) (W : H ≃ₗᵢ[ℂ] H) (ψ : H) (h : ψ ∈ (generator fun (t : ℝ) => (W.symm.trans (U t)).trans W).domain) (h' : W.symm ψ ∈ (generator U).domain) : ↑(generator fun (t : ℝ) => (W.symm.trans (U t)).trans W) ⟨ψ, h⟩ = W (↑(generator U) ⟨W.symm ψ, h'⟩)

The generator of t ↦ W U(t) W⁻¹ is W A W⁻¹, A the generator of U.

Blueprint reference: lmm:generator-conj.