Physlib

PhyslibAlpha.ProbabilisticTheory.Dynamics.OneParameterGroup

One-parameter groups

i. Overview

A one-parameter group is a family `α : ℝ → E → E` with `α 0 = id` and `α (s + t) = α s ∘ α t`. It is stated for an arbitrary type `E`; preservation of structure and continuity are separate conditions.

ii. Key results

  • `IsOneParameterGroup` : one-parameter groups.

iii. Table of contents

  • A. The group law

A. The group law

3 declarations

theorem

α(−t)\alpha(-t) is the left inverse of α(t)\alpha(t) for a one-parameter group

Let α:R→E→E\alpha: \mathbb{R} \to E \to E be a one-parameter group on a type EE, satisfying the group law α(s+t)=α(s)∘α(t)\alpha(s + t) = \alpha(s) \circ \alpha(t) and α(0)=id\alpha(0) = \text{id}. For any time t∈Rt \in \mathbb{R} and any element a∈Ea \in E, the map α(−t)\alpha(-t) acts as a left inverse to α(t)\alpha(t), such that α(−t)(α(t)(a))=a\alpha(-t)(\alpha(t)(a)) = a.

theorem

α(t)(α(−t)a)=a\alpha(t)(\alpha(-t)a) = a for one-parameter groups

Let α:R→E→E\alpha : \mathbb{R} \to E \to E be a one-parameter group. For any t∈Rt \in \mathbb{R} and any a∈Ea \in E, it holds that α(t)(α(−t)a)=a\alpha(t)(\alpha(-t)a) = a.

theorem

α(t)\alpha(t) is bijective for a one-parameter group

Let EE be a type and α:R→E→E\alpha: \mathbb{R} \to E \to E be a one-parameter group satisfying α(0)=idE\alpha(0) = \text{id}_E and α(s+t)=α(s)∘α(t)\alpha(s + t) = \alpha(s) \circ \alpha(t) for all s,t∈Rs, t \in \mathbb{R}. Then for any t∈Rt \in \mathbb{R}, the mapping α(t)\alpha(t) is bijective.