On the other hand, the exp-style is sometimes more convenient for inline equations, and is necessary on the rare occasions when there is a real distinction to be made.
(1) To compute the differential dexp of exp at X, dexpX: TgX → TGexp(X), the standard recipe[2] is employed.
This means that the exponential mapping from the Lie algebra to the matrix Lie group is given by the usual power series, i.e. matrix exponentiation.
The conclusion of the proof still holds in the general case, provided each occurrence of exp is correctly interpreted.
The outline of proof makes use of the technique of differentiation with respect to s of the parametrized expression to obtain a first order differential equation for Γ which can then be solved by direct integration in s. The solution is then eX Γ(1, t).
Lemma Let Ad denote the adjoint action of the group on its Lie algebra.
Integration yields Using the formal power series to expand the exponential, integrating term by term, and finally recognizing (2), and the result follows.
[8] The formula in the general case is given by[9] where[nb 2] which formally reduces to Here the exp-notation is used for the exponential mapping of the Lie algebra and the calculus-style notation in the fraction indicates the usual formal series expansion.
For more information and two full proofs in the general case, see the freely available Sternberg (2004) reference.
By direct differentiation of the standard limit definition of the exponential, and exchanging the order of differentiation and limit, where each factor owes its place to the non-commutativity of X(t) and X´(t).
Dividing the unit interval into N sections Δs = Δk/N (Δk = 1 since the sum indices are integers) and letting N → ∞, Δk → dk, k/N → s, Σ → ∫ yields The inverse function theorem together with the derivative of the exponential map provides information about the local behavior of exp.
If g is an analytic function of a complex variable expressed in a power series such that g(U) for a matrix U converges, then the eigenvalues of g(U) will be g(λij), where λij are the eigenvalues of U, the double subscript is made clear below.
Putting 1 − exp(−λij)/λij = 0 one sees that dexp is invertible precisely when The eigenvalues of adX are, in turn, related to those of X.
Fix an ordered basis ei of the underlying vector space V such that X is lower triangular.
This means that adX is lower triangular with its eigenvalues λij = λi − λj on the diagonal.
The conclusion is that dexpX is invertible, hence exp is a local bianalytical bijection around X, when the eigenvalues of X satisfy[10][nb 4] In particular, in the case of matrix Lie groups, it follows, since dexp0 is invertible, by the inverse function theorem that exp is a bi-analytic bijection in a neighborhood of 0 ∈ g in matrix space.
Furthermore, exp, is a bi-analytic bijection from a neighborhood of 0 ∈ g in g to a neighborhood of e ∈ G.[11] The same conclusion holds for general Lie groups using the manifold version of the inverse function theorem.
It also follows from the implicit function theorem that dexpξ itself is invertible for ξ sufficiently small.
Thus, and hence, formally,[13][14] However, using the relationship between Ad and ad given by (4), it is straightforward to further see that and hence Putting this into the form of an integral in t from 0 to 1 yields, an integral formula for Z(1) that is more tractable in practice than the explicit Dynkin's series formula due to the simplicity of the series expansion of ψ.
Note this expression consists of X+Y and nested commutators thereof with X or Y.
A textbook proof along these lines can be found in Hall (2015) and Miller (1972).
Dynkin's formula mentioned may also be derived analogously, starting from the parametric extension whence so that, using the above general formula, Since, however, the last step by virtue of the Mercator series expansion, it follows that and, thus, integrating, It is at this point evident that the qualitative statement of the BCH formula holds, namely Z lies in the Lie algebra generated by X, Y and is expressible as a series in repeated brackets (A).
For each k, terms for each partition thereof are organized inside the integral ∫dt tk−1.
For a similar proof with detailed series expansions, see Rossmann (2002).
Change the summation index in (5) to k = n − 1 and expand in a power series.
To handle the series expansions simply, consider first Z = log(eXeY).
(99) where Sk is the set of all sequences s = (i1, j1, ..., ik, jk) of length 2k subject to the conditions in (99).
Equation (99) then gives or, with a switch of notation, see An explicit Baker–Campbell–Hausdorff formula, Note that the summation index for the rightmost eadtX in the second term in (97) is denoted ik + 1, but is not an element of a sequence s ∈ Sk.
The striking similarity with (99) is not accidental: It reflects the Dynkin–Specht–Wever map, underpinning the original, different, derivation of the formula.
[15] Namely, if is expressible as a bracket series, then necessarily[18] Putting observation (A) and theorem (B) together yields a concise proof of the explicit BCH formula.