Physlib

Physlib.Mathematics.OneParameterSubgroups.Basic

One-parameter subgroups of real Banach algebras

i. Overview

Let `E` be a real Banach algebra. This file proves that every continuous additive character `U : AddChar ℝ E` has the form `U(t) = exp (t • A)`, where `A = deriv U 0`.

This is the Banach-algebra argument underlying the correspondence between norm-continuous unitary one-parameter groups and bounded self-adjoint generators. See `Physlib.Mathematics.OneParameterSubgroups.Unitary` for that correspondence.

**Proof outline.** Continuity at zero implies that, for sufficiently small `d > 0`, the integral of `U` over `[0, d]` is close to `d • 1` and therefore invertible. If `I` is the indefinite integral of `U`, the homomorphism law gives `U(t) * I(d) = I(t + d) - I(t)`. This identity proves that `U` is differentiable. Setting `A` to the derivative at zero then gives the differential equation `U'(t) = U(t)A`. Consequently `U(t) * exp (-tA)` has zero derivative and is constant. Uniqueness follows by differentiating two exponential representations at zero.

ii. Key results

* `OneParameterSubgroup.apply_eq_exp_smul_deriv`: A continuous one-parameter subgroup is the exponential of its derivative at zero. * `OneParameterSubgroup.generator_unique`: Any exponential generator equals the derivative at zero.

iii. References

6 declarations

instance

Q\mathbb{Q}-normed algebra structure for EE

For a real normed algebra EE, this definition provides the structure of a normed algebra over the rational numbers Q\mathbb{Q} by restricting the scalars from R\mathbb{R} to Q\mathbb{Q}. This instance is used to satisfy the requirements of the exponential map exp⁡(x)=∑n=0∞xnn!\exp(x) = \sum_{n=0}^\infty \frac{x^n}{n!}, which requires the ability to multiply by rational coefficients 1n!\frac{1}{n!}.

theorem

Existence of an invertible interval integral for continuous one-parameter subgroups

Let EE be a nontrivial real Banach algebra and let U:R→EU : \mathbb{R} \to E be a continuous additive character (a one-parameter subgroup satisfying U(s+t)=U(s)U(t)U(s+t) = U(s)U(t)). There exists a positive real number d>0d > 0 such that the integral of UU over the interval [0,d][0, d], denoted by ∫0dU(x) dx\int_0^d U(x) \, dx, is an invertible element (a unit) in EE.

theorem

U(s)∫0tU=∫0s+tU−∫0sUU(s) \int_{0}^{t} U = \int_{0}^{s+t} U - \int_{0}^{s} U for continuous one-parameter subgroups

Let EE be a real Banach algebra and U:R→EU: \mathbb{R} \to E be a continuous additive character (a one-parameter subgroup satisfying U(s+t)=U(s)U(t)U(s+t) = U(s)U(t)). For any s,t∈Rs, t \in \mathbb{R}, the product of U(s)U(s) and the integral of UU over [0,t][0, t] is equal to the difference of the integrals of UU over [0,s+t][0, s+t] and [0,s][0, s]: U(s)∫0tU(x) dx=∫0s+tU(x) dx−∫0sU(x) dxU(s) \int_{0}^{t} U(x) \, dx = \int_{0}^{s+t} U(x) \, dx - \int_{0}^{s} U(x) \, dx

theorem

A continuous one-parameter subgroup is differentiable

Let EE be a nontrivial real Banach algebra and U:R→EU : \mathbb{R} \to E be a continuous one-parameter subgroup (i.e., a continuous map satisfying U(s+t)=U(s)⋅U(t)U(s + t) = U(s) \cdot U(t) for all s,t∈Rs, t \in \mathbb{R}). Then UU is differentiable on R\mathbb{R}.

theorem

Continuous one-parameter subgroups are given by U(t)=exp⁡(t⋅U′(0))U(t) = \exp(t \cdot U'(0))

Let EE be a real Banach algebra. If U:R→EU: \mathbb{R} \to E is a continuous one-parameter subgroup (that is, a continuous map satisfying U(s+t)=U(s)U(t)U(s+t) = U(s)U(t) for all s,t∈Rs, t \in \mathbb{R} and U(0)=1U(0) = 1), then for any t∈Rt \in \mathbb{R}, the value of UU is given by U(t)=exp⁡(t⋅U′(0))U(t) = \exp(t \cdot U'(0)) where U′(0)U'(0) denotes the derivative of UU at t=0t=0 and exp⁡\exp is the exponential function in the Banach algebra EE.

theorem

The generator AA of U(t)=exp⁡(tA)U(t) = \exp(tA) is U′(0)U'(0)

Let EE be a real Banach algebra. If U:R→EU : \mathbb{R} \to E is a one-parameter subgroup (an additive character) such that U(t)=exp⁡(tA)U(t) = \exp(t A) for some A∈EA \in E and all t∈Rt \in \mathbb{R}, then AA is equal to the derivative of UU at zero, denoted U′(0)U'(0).