Derivatives involving the local Lie logarithm #
This file records first-order interactions between the local logarithm, the exponential, and group multiplication.
Main result #
hasDerivAt_mulInvariantLog_mulInvariantExp_smul_mul_mulInvariantExp_smul: the local logarithm of the product of two exponential lines has initial derivativeX + Y.
theorem
hasDerivAt_mulInvariantLog_mulInvariantExp_smul_mul_mulInvariantExp_smul
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{H : Type u_2}
[TopologicalSpace H]
{I : ModelWithCorners ℝ E H}
{G : Type u_3}
[TopologicalSpace G]
[ChartedSpace H G]
[Group G]
[FiniteDimensional ℝ E]
[LieGroup I (↑⊤) G]
[T2Space G]
[BoundarylessManifold I G]
(X Y : GroupLieAlgebra I G)
:
HasDerivAt
(fun (t : ℝ) =>
have this := mulInvariantLog (mulInvariantExp (t • X) * mulInvariantExp (t • Y));
this)
((have this := X;
this) + have this := Y;
this)
0
The local logarithm of the product of two exponential lines has initial derivative X + Y.