PhyslibAlpha.AlgebraicFramework.Dynamics.Generator

The infinitesimal generator of a one-parameter group

i. Overview

A generator is analytic/dynamical, not algebraic: `D a := lim_{t→0} (α_t(a) - a)/t`, requiring a topology on `E` (here, a normed real vector space — enough to make sense of the limit) but *not* requiring `E` to carry any multiplication, order, or star structure at all. This is the deliberate converse emphasis of `Algebra/Derivation.lean`: derivation is pure algebra with no analysis; generator is pure analysis with no algebra. `GeneratorIsDerivation.lean` is the bridge connecting the two, once `E` happens to also carry a compatible multiplication.

`IsGenerator` is phrased via `HasDerivAt` rather than `deriv` directly, which keeps every downstream theorem a clean implication (`differentiable ⇒ conclusion`) instead of needing to first discharge a `DifferentiableAt` side goal to unfold `deriv`.

ii. Key definitions and results

- `IsGenerator` - `IsGenerator.unique` : the generator, if it exists, is unique (immediate from uniqueness of derivatives)

iii. Table of contents

A. The generator

A. The generator

2 declarations

definition

$D$ is the infinitesimal generator of $\alpha$

#IsGenerator

For a one-parameter family of maps $\alpha: \mathbb{R} \to E \to E$ on a normed real vector space $E$ , the predicate `IsGenerator α D` holds if for every $a \in E$ , the map $t \mapsto \alpha(t) a$ is differentiable at $t = 0$ and its derivative is $D(a)$ .

theorem

The infinitesimal generator of a one-parameter family is unique

#unique

Let $E$ be a normed real vector space and $\alpha: \mathbb{R} \to (E \to E)$ be a one-parameter family of maps. If $D_1, D_2: E \to E$ are both infinitesimal generators of $\alpha$ , then $D_1 = D_2$ . (A map $D: E \to E$ 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)$ .)