How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Baker–Campbell–Hausdorff theorem
Statement
Assume . Let be a finite-dimensional real Lie group with Lie algebra . For every chosen local logarithm there is an open neighborhood of in such that Dynkin's series converges for and
Consequently, for every ,
The neighborhood can be chosen inside any convergence ball supplied by the preceding convergence lemma and so that the product remains in the fixed domain of .
Facts & Assumptions
Given: , a finite-dimensional real Lie group , a fixed norm on , and one local logarithm associated with .
The local logarithm is the inverse of the exponential on the specified open neighborhoods, and Dynkin's BCH series converges absolutely on a sum-norm ball and uniformly on smaller closed balls. Local logarithm on a Lie group. Local convergence of the Baker–Campbell–Hausdorff series.
Right-trivialization of is the entire operator series , and the linear-ODE exponential is its operator power series, uniformly on compact parameter intervals. Right-trivialized differential of the Lie-group exponential.
The adjoint map is a smooth representation and, assuming countable choice, . The Axiom of Countable Choice (). Adjoint is a smooth Lie-group representation. Adjoint exponential identity.
The curve is the integral curve of through ; translations give the tangent trivializations; and differentials obey the chain rule. One-parameter subgroups are integral curves of left-invariant fields. Left and right translations on a Lie group. The chain rule for differentials of smooth maps.
Formal exponential and logarithm over a commutative rational algebra are inverse, where . Formal exponential, logarithm, and binomial powers over a commutative -algebra. Formal and are inverse homomorphisms and formal binomial powers obey the expected addition laws.
The scalar exponential series converges everywhere, and a geometric series converges when its ratio has absolute value less than one. The exponential series converges absolutely for every real argument. For , , and for the series diverges.
The tube lemma supplies one neighborhood uniform over a compact parameter set. A finite basis gives bounded coordinates; uniform scalar limits commute with Riemann integration; and vector-valued FTC is componentwise. Tube lemma: if is compact and an open contains , then contains for some open . A chosen algebraic basis identifies a finite-dimensional normed space with a coordinate space. A uniform limit of Riemann-integrable functions is Riemann integrable, and its integral is the limit of their integrals. If is differentiable with integrable then ; and a bounded derivative makes Lipschitz.
Proof
By [F1], choose a BCH convergence ball. The smooth map sends to . Apply the tube lemma to and intersect the resulting neighborhood of with a sufficiently small sum-norm ball. For in this neighborhood, put and ; then is smooth, , and for all .
Right-trivializing the derivative of the product and using the two one-parameter-subgroup equations gives . Applying [F2] to therefore gives , where and .
Since is a representation, [F3] and step 1.1 give . Put . Continuity and the tube lemma allow a further shrinking, uniform in , so that and remains in a fixed small coordinate ball.
Define . It converges absolutely for by [F6]. In the commutative formal subalgebra generated by one indeterminate , [F5] gives , hence . Absolute operator convergence permits substitution and coefficientwise multiplication, so is the two-sided inverse of . Thus step 2.1 becomes .
Expand by [F2]: . The bound , together with exponential scalar majorants after one further shrinking, makes the expansions in step 3.1 jointly absolutely and uniformly convergent on . In finite coordinates [F7] therefore permits termwise multiplication, regrouping, and integration.
A term with positive blocks from followed by the terminal has word degree , coefficient , and power ; a term followed by has the same description, with final block and again power . Every other possible final block in Dynkin's formula has at least two terminal equal letters and its right-nested commutator is zero. Hence integration from zero to one contributes the factor and gives exactly the full degree- Dynkin polynomial .
By vector-valued FTC and step 1.1, . Steps 4.1–5.1 and the uniform convergence in [F1] identify this integral with . Since , the logarithmic identity follows; applying and using [F1] gives the asserted product identity.
A Lie group contains its identity. In dimension zero the identities are the unique identities, and in dimension one the bracket vanishes so BCH is and the local product is additive in exponential coordinates. No adjoint endomorphism is assumed invertible: step 3.1 inverts by a convergent series and never divides by . Both endpoints of occur in steps 1.1 and 6.1. The only choice principle is , inherited exactly through the local logarithm, exponential, and adjoint-exponential suppliers in [F1]–[F4]; all shrinkings select finitely many single witnesses. No metric independence beyond the arbitrary auxiliary norm and no biconditional is asserted.
Depends on
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
- Local logarithm on a Lie group
- Local convergence of the Baker–Campbell–Hausdorff series
- Right-trivialized differential of the Lie-group exponential
- Adjoint is a smooth Lie-group representation
- Adjoint exponential identity
- One-parameter subgroups are integral curves of left-invariant fields
- Left and right translations on a Lie group
- Formal exponential, logarithm, and binomial powers over a commutative $\mathbb Q$-algebra
- Formal $\exp$ and $\log$ are inverse homomorphisms and formal binomial powers obey the expected addition laws
- The exponential series converges absolutely for every real argument
- For $|r| < 1$, $\sum_{k \ge 0} r^k = 1/(1-r)$, and for $|r| \ge 1$ the series diverges
- Tube lemma: if $K$ is compact and an open $N \subseteq X \times Z$ contains $K \times \{z_0\}$, then $N$ contains $K \times W$ for some open $W \ni z_0$
- A chosen algebraic basis identifies a finite-dimensional normed space with a coordinate space
- A uniform limit of Riemann-integrable functions is Riemann integrable, and its integral is the limit of their integrals
- If $f : [a,b] \to \mathbb{R}^m$ is differentiable with integrable $f'$ then $\int_a^b f' = f(b)-f(a)$; and a bounded derivative makes $f$ Lipschitz
- The chain rule for differentials of smooth maps
Used by
Dependency tree · two levels
107 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Michael Müger, Notes on the Baker-Campbell-Hausdorff-Dynkin theorem (standard reference, not scraped)
- Anthony W. Knapp, Lie Groups Beyond an Introduction, 2nd ed. (standard reference, not scraped)
- Alexander Kirillov Jr., An Introduction to Lie Groups and Lie Algebras (standard reference, not scraped)