6 One-parameter subgroups of affine isomorphisms

Lemma 6.1 Functional equation in one parameter subgroups of affine isomorphisms

Suppose that \(t \mapsto A_t\) is a homomorphism of multiplicative groups \((0,+\infty ) \to \mathrm{Aff}^+_{\mathbb {R}}\), i.e., for any \(s, t {\gt} 0\) we have

\begin{align*} A_{s t} = A_s \circ A_t . \end{align*}

Write \(A_t(x) = a_t x + b_t\), with \(a_t {\gt} 0\) and \(b_t \in \mathbb {R}\). Then we have, for any \(s, t {\gt} 0\),

\begin{align*} a_{t s} = \; & a_t \, a_s \qquad \text{ and } \\ b_{t s} = \; & a_t \, b_s + b_t . \end{align*}

(Also by symmetry \(b_{t s} = a_s \, b_t + b_s\).)

Proof ▶

Lemma 6.2 Functional equation scaling coefficient solution

Suppose that \(a \colon (0,+\infty ) \to (0,+\infty )\) is a measurable function satisfying, for any \(s, t {\gt} 0\),

\begin{align*} a(t s) = \; & a(t) \, a(s) . \end{align*}

Then there exists a \(\rho \in \mathbb {R}\) such that for all \(t {\gt} 0\),

\begin{align*} a(t) = t^{\rho } . \end{align*}

Proof ▶

Lemma 6.3 Functional equation translation coefficient solution with \(\rho = 0\)

Suppose that \(b \colon (0,+\infty ) \to \mathbb {R}\) is a measurable function satisfying, for any \(s, t {\gt} 0\),

\begin{align*} b(t s) = \; & b(s) + b(t) . \end{align*}

Then there exists a constant \(c\) such that for \(t \in (0,+\infty )\) we have

\begin{align*} b(t) = \; & -c \, \log (t) . \end{align*}

Proof ▶

Lemma 6.4 Functional equation translation coefficient solution with \(\rho \ne 0\)

Suppose that \(\rho \in \mathbb {R}\setminus \left\{ 0 \right\} \) and \(b \colon (0,+\infty ) \to \mathbb {R}\) is a measurable function satisfying, for any \(s, t {\gt} 0\),

\begin{align*} b(t s) = \; & t^{\rho } \, b(s) + b(t) . \end{align*}

Then there exists a constant \(c\) such that for \(t \in (0,+\infty ) \setminus \left\{ 1 \right\} \) we have

\begin{align*} b(t) = \; & c (1 - t^{-\rho }) . \end{align*}

Proof ▶

The above solutions to functional equations can be used to classify all one-parameter subgroups of the group of oriented affine isomorphisms of \(\mathbb {R}\). Such a subgroup can be given in a parametrized form as a group homomorphism \(\mathbb {R}\to \mathrm{Aff}^+_{\mathbb {R}}\) (from the additive group \(\mathbb {R}\)) or alternatively as group homomorphisms \((0,+\infty ) \to \mathrm{Aff}^+_{\mathbb {R}}\) (from the multiplicative group \((0,+\infty )\)). The additive and multiplicative versions are related by the change of variable \(\mathbb {R}\ni t \leftrightarrow \lambda := e^t \in (0,+\infty )\) (conversely, \(t = \log (\lambda )\)). (In Lean the type \(\mathbb {R}\) is more convenient than the type \((0,+\infty )\), so in formal statements we prefer the former choice.)

Theorem 6.5 One-parameter subgroups of affine isomorphisms of \(\mathbb {R}\)

[TODO: Switch to additive notation and \(\mathbb {R}\) rather than multiplicative notation and \((0,+\infty )\), to match the most convenient formalized statements.]

Suppose that \(t \mapsto A_t\) is a measurable homomorphism of multiplicative groups \((0,+\infty ) \to \mathrm{Aff}^+_{\mathbb {R}}\), i.e., for any \(s, t {\gt} 0\) we have

\begin{align*} A_{s t} = A_s \circ A_t \end{align*}

and \(A_t(x) = a_t x + b_t\), with \(t \mapsto a_t\) and \(t \mapsto b_t\) measurable functions. Then either

(0)

there exists a \(\beta \in \mathbb {R}\) such that for all \(t {\gt} 0\) and \(x \in \mathbb {R}\)

\begin{align*} A_t(x) = x + \beta \, \log (t) ; \end{align*}

(1)

there exists a \(\rho \ne 0\) and \(c \in \mathbb {R}\) such that for all \(t {\gt} 0\) and \(x \in \mathbb {R}\)

\begin{align*} A_t(x) = t^{\rho } (x - c) + c . \end{align*}

Proof ▶