PhyslibAlpha.AlgebraicFramework.Dynamics.GeneratorIsDerivation

The generator of a one-parameter automorphism group is a derivation

i. Overview

**The bridge theorem.** Given a continuous (bounded) bilinear multiplication on a normed space `E`, and a one-parameter family `α : ℝ → E → E` that (a) fixes `0` at `t = 0` in the sense `α 0 = id`, and (b) preserves the product at every time (`α t (a * b) = α t a * α t b`), the generator of `α` — purely analytically defined, `Dynamics/Generator.lean` — automatically satisfies the Leibniz rule, hence is a derivation in the purely algebraic sense of `Algebra/Derivation.lean`: $D(a \circ b) = D(a) \circ b + a \circ D(b).$

This is deliberately proved at the most general level where the argument is legitimate: no order, no Jordan identity, no star structure, not even associativity or commutativity of `*` — only that `*` is `ℝ`-bilinear and *bounded* (`IsBoundedBilinearMap`), which is exactly what lets one differentiate `t ↦ α t a * α t b` via the product rule for bilinear maps (`IsBoundedBilinearMap.hasFDerivAt`) and read off the Leibniz rule from `α`'s multiplicativity. In particular `IsCommJordan` never appears in this file: it is one instance of the hypothesis `hmul`/`IsBoundedBilinearMap`, reached only by later composing this theorem with a JB-algebra's submultiplicativity axiom (`‖a ∘ b‖ ≤ ‖a‖‖b‖`, `JB/Basic.lean`) — see the module docstring's closing remark for exactly how that composition goes, deliberately *not* performed in this file.

ii. Key definitions and results

`IsGenerator.isDerivation_of_isAutomorphismFamily`

iii. Table of contents

A. The bridge theorem

A. The bridge theorem

1 declaration

theorem

The generator of a one-parameter automorphism family is a derivation

#isDerivation_of_isAutomorphismFamily

Let $E$ be a normed real vector space equipped with a multiplication operation $(a, b) \mapsto a \cdot b$ that is a bounded $\mathbb{R}$ -bilinear map. Let $\alpha: \mathbb{R} \to E \to E$ be a one-parameter family of maps such that: 1. $\alpha(0)$ is the identity map, i.e., $\alpha(0)a = a$ for all $a \in E$ . 2. For every $t \in \mathbb{R}$ , $\alpha(t)$ preserves the multiplication, i.e., $\alpha(t)(a \cdot b) = \alpha(t)a \cdot \alpha(t)b$ for all $a, b \in E$ . If $D: E \to E$ is a linear map that is the generator of $\alpha$ (meaning $D(a) = \left. \frac{d}{dt} \right|_{t=0} \alpha(t)a$ for all $a \in E$ ), then $D$ is a derivation. That is, $D$ satisfies the Leibniz rule: $D(a \cdot b) = D(a) \cdot b + a \cdot D(b)$ for all $a, b \in E$ .