Physicslib4.Spectral.Stone.Exponential

Exponentiating a self-adjoint operator

For a self-adjoint operator A, the functional calculus applied to the bounded functions λ ↦ e^{itλ} gives a strongly continuous one-parameter unitary group t ↦ e^{itA} whose infinitesimal generator is A (blueprint §10.4.3, Proposition prpstn:hall-10.14).

Main definitions

• expFun t — the function λ ↦ e^{itλ} on ℝ.
• expUnitary hA t — the unitary e^{itA}, the bounded integral of expFun t against the spectral measure of A.

Main statements

• isOneParameterUnitaryGroup_expUnitary, isStronglyContinuous_expUnitary.
• tendsto_generatorQuotient_expUnitary — the derivative of e^{itA} at 0 on Dom(A).
• generator_expUnitary — the generator of t ↦ e^{itA} is A.

noncomputable def Physicslib4.Spectral.Stone.expFun (t x : ℝ) : ℂ

The function f_t(λ) = e^(itλ) on ℝ, whose functional calculus is the unitary e^(itA).

For each real t it is continuous and of modulus 1, hence bounded and measurable (expFun_mem_bddMeasurable), so f_t(A) is a bounded operator for every self-adjoint A. On an eigenvector of A with eigenvalue λ, e^(itA) acts as multiplication by the phase e^(itλ).

Implementation note: the function is Complex.exp (Complex.I * ((t * x : ℝ) : ℂ)), the product tλ formed in ℝ and then cast to ℂ.

Blueprint: def:exp-unitary-group

Equations

• Physicslib4.Spectral.Stone.expFun t x = Complex.exp (Complex.I * ↑(t * x))

theorem Physicslib4.Spectral.Stone.expFun_mem_bddMeasurable (t : ℝ) : expFun t ∈ BddMeasurable ℝ

f_t is bounded and measurable.

theorem Physicslib4.Spectral.Stone.integral_expFun_mem_unitary {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (μ : ProjectionValuedMeasure ℝ H) (t : ℝ) : μ.integral (expFun t) ∈ unitary (H →L[ℂ] H)

For a projection-valued measure μ on ℝ (in particular the spectral measure of a self-adjoint operator), the bounded integral of f_t(λ) = e^{itλ} is unitary.

Blueprint reference: lmm:exp-unitary.

noncomputable def Physicslib4.Spectral.Stone.expUnitary {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →ₗ.[ℂ] H} (hA : IsSelfAdjoint A) (t : ℝ) : H ≃ₗᵢ[ℂ] H

The unitary operator e^(itA) of a self-adjoint operator A, defined by the spectral theorem as ∫ e^(itλ) dμ(A)(λ).

When A is unbounded the exponential series makes no sense, since Aⁿψ need not be defined. The spectral theorem replaces it: e^(itA) integrates the function e^(itλ) against the spectral measure μ(A). Because |e^(itλ)| = 1 the result is a bounded operator defined on all of H, and it is unitary (integral_expFun_mem_unitary). As a function of t it is a strongly continuous one-parameter unitary group (isOneParameterUnitaryGroup_expUnitary, isStronglyContinuous_expUnitary) with infinitesimal generator A (generator_expUnitary). For a Hamiltonian Ĥ, the time evolution operator e^(−itĤ) is this unitary at the parameter −t.

Implementation note: the operator is the bounded integral ProjectionValuedMeasure.integral of expFun t against Unbounded.spectralMeasure hA, made an element of H ≃ₗᵢ[ℂ] H by Unitary.linearIsometryEquiv. That it is the functional calculus f_t(A) is functionalCalculus_expFun. The definition takes the proof hA of self-adjointness as an argument, which is why stone states self-adjointness of the generator as an existential.

Blueprint: def:exp-unitary-group

Equations

• Physicslib4.Spectral.Stone.expUnitary hA t = Unitary.linearIsometryEquiv ⟨(Physicslib4.Spectral.Unbounded.spectralMeasure hA).integral (Physicslib4.Spectral.Stone.expFun t), ⋯⟩

theorem Physicslib4.Spectral.Stone.expUnitary_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →ₗ.[ℂ] H} (hA : IsSelfAdjoint A) (t : ℝ) (ψ : H) : (expUnitary hA t) ψ = ((Unbounded.spectralMeasure hA).integral (expFun t)) ψ

theorem Physicslib4.Spectral.Stone.functionalCalculus_expFun {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →ₗ.[ℂ] H} (hA : IsSelfAdjoint A) (t : ℝ) : Unbounded.functionalCalculus hA (expFun t) = (expUnitary hA t).toLinearIsometry.toPMap ⊤

The unitary e^(itA) is the functional calculus f_t(A) of f_t(λ) = e^(itλ), an operator defined on all of H.

The functional calculus Unbounded.functionalCalculus allows unbounded functions and produces operators with a domain; for a bounded function such as f_t it agrees with the bounded integral that defines expUnitary (functionalCalculus_of_bddMeasurable). This identification is what lets results about bounded integrals against a projection-valued measure be used for e^(itA).

Implementation note: the statement is an equality of LinearPMaps, with e^(itA) on the domain ⊤ = H.

Blueprint: def:exp-unitary-group

theorem Physicslib4.Spectral.Stone.isOneParameterUnitaryGroup_expUnitary {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →ₗ.[ℂ] H} (hA : IsSelfAdjoint A) : IsOneParameterUnitaryGroup (expUnitary hA)

The group law: e^{i0A} = 1 and e^{i(s+t)A} = e^{isA} e^{itA}.

Blueprint reference: lmm:exp-group-law.

theorem Physicslib4.Spectral.Stone.isStronglyContinuous_expUnitary {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →ₗ.[ℂ] H} (hA : IsSelfAdjoint A) : IsStronglyContinuous (expUnitary hA)

t ↦ e^{itA} is strongly continuous.

Blueprint reference: lmm:exp-strongly-continuous.

theorem Physicslib4.Spectral.Stone.functionalCalculus_sub_of_bddMeasurable {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →ₗ.[ℂ] H} (hA : IsSelfAdjoint A) {f g : ℝ → ℂ} (hf : Measurable f) (hg : g ∈ BddMeasurable ℝ) : Unbounded.functionalCalculus hA (g - f) = Unbounded.functionalCalculus hA g - Unbounded.functionalCalculus hA f

Subtracting an unbounded function from a bounded one: for measurable f and bounded measurable g, (g - f)(A) = g(A) - f(A) as unbounded operators. The domain of the right side is H ⊓ W_f = W_f, so this says both W_{g - f} = W_f and (g - f)(A) ψ = g(A) ψ - f(A) ψ on W_f.

Blueprint reference: lmm:functional-calculus-sub-bounded.

theorem Physicslib4.Spectral.Stone.norm_sq_generatorQuotient_expUnitary_sub {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →ₗ.[ℂ] H} (hA : IsSelfAdjoint A) (ψ : ↥A.domain) (t : ℝ) : ‖generatorQuotient (expUnitary hA) (↑ψ) t - ↑A ψ‖ ^ 2 = ∫ (x : ℝ), ‖(Complex.I * ↑t)⁻¹ * (expFun t x - 1) - ↑x‖ ^ 2 ∂(Unbounded.spectralMeasure hA).assoc ↑ψ

The norm identity for the difference quotient: for ψ ∈ Dom(A) and every t, with g_t(λ) = (1/i)(e^{itλ} - 1)/t, ‖(1/i)(e^{itA}ψ - ψ)/t - Aψ‖² = ∫ |g_t(λ) - λ|² dμ^A_ψ(λ). The blueprint states it for t ≠ 0; it also holds at t = 0, where both sides are ‖Aψ‖² by the convention 0⁻¹ = 0, so no hypothesis on t is needed.

Blueprint reference: lmm:exp-quotient-norm-identity.

theorem Physicslib4.Spectral.Stone.tendsto_generatorQuotient_expUnitary {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →ₗ.[ℂ] H} (hA : IsSelfAdjoint A) (ψ : ↥A.domain) : Filter.Tendsto (generatorQuotient (expUnitary hA) ↑ψ) (nhdsWithin 0 {0}ᶜ) (nhds (↑A ψ))

The derivative of e^{itA} at 0: for ψ ∈ Dom(A), (1/i)(e^{itA}ψ - ψ)/t → Aψ as t → 0, t ≠ 0.

Blueprint reference: lmm:exp-derivative-at-zero.

theorem Physicslib4.Spectral.Stone.generator_expUnitary {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {A : H →ₗ.[ℂ] H} (hA : IsSelfAdjoint A) : IsOneParameterUnitaryGroup (expUnitary hA) ∧ IsStronglyContinuous (expUnitary hA) ∧ generator (expUnitary hA) = A

Exponentiating a self-adjoint operator: for self-adjoint A, t ↦ e^(itA) is a strongly continuous one-parameter unitary group whose infinitesimal generator is A, domains included.

This is the easier half of the correspondence between self-adjoint operators and strongly continuous one-parameter unitary groups; Stone's theorem (stone) is the other half. For ψ in Dom(A) the difference quotient (1/i)(e^(itA)ψ − ψ)/t tends to Aψ (tendsto_generatorQuotient_expUnitary), so the generator extends A. The generator is symmetric (isSymmetric_generator), and a self-adjoint operator has no proper symmetric extension (eq_of_isSelfAdjoint_of_isSymmetric_of_le), so the generator is A. In particular Dom(A) is exactly the set of ψ for which the difference quotient converges.

Implementation note: the first two conjuncts are point 1 of the blueprint proposition; the third, the equality generator (expUnitary hA) = A of LinearPMaps, is points 2 and 3 together. Strong continuity and the limit of the difference quotient are proved from norm identities that write ‖e^(isA)ψ − e^(itA)ψ‖² and the squared error of the difference quotient as integrals against the spectral distribution of ψ, and from dominated convergence in its filter form (tendsto_integral_filter_of_dominated_convergence).

Blueprint: prpstn:hall-10.14