PhyslibAlpha.ProbabilisticTheory.Dynamics.Generator

Generators of one-parameter groups

i. Overview

The generator of a one-parameter family `α` on a normed space is `D a = lim_{t → 0} (α t a - a) / t`, stated with `HasDerivAt`. It needs a topology but no algebraic structure, and it is unique when it exists.

ii. Key results

`IsGenerator` : `D` generates `α`.
`IsGenerator.unique` : the generator is unique.

iii. Table of contents

A. The generator

A. The generator

2 declarations

definition

$D$ is the infinitesimal generator of $\alpha$ at $t = 0$

#IsGenerator

Let $E$ be a normed space. For a one-parameter family of maps $\alpha: \mathbb{R} \to E \to E$ and a map $D: E \to E$ , $D$ is the infinitesimal generator of $\alpha$ if for every $a \in E$ , the map $t \mapsto \alpha(t, a)$ is differentiable at $t = 0$ with derivative $D(a)$ . This is expressed as $\left. \frac{d}{dt} \alpha(t, a) \right|_{t=0} = D(a)$ .

theorem

The infinitesimal generator of a one-parameter family is unique

#unique

Let $E$ be a normed space and $\alpha: \mathbb{R} \to E \to E$ be a one-parameter family of maps. If $D_1: E \to E$ and $D_2: E \to E$ are both infinitesimal generators of $\alpha$ , such that for every $a \in E$ , the derivative of the map $t \mapsto \alpha(t, a)$ at $t = 0$ is equal to both $D_1(a)$ and $D_2(a)$ , then $D_1 = D_2$ .