Parameter dependence of invariant integral curves

This file begins the analytic parameter-dependence theory for the invariant integral curves that define the Lie-group exponential. In the identity chart, the tangent vector and group coordinate form an autonomous ODE on the product model space. Picard--Lindelöf then supplies a single local solution family, continuous jointly in its initial condition and time, for all sufficiently small tangent vectors.

Main results

• mulInvariantCoordinateVectorField: the invariant vector field in the identity chart, with its generating tangent vector included as a parameter.
• contDiffAt_mulInvariantCoordinateVectorField: this coordinate vector field is C^n at every generating vector over the identity coordinate when multiplication is C^(n + 1).
• mulInvariantCoordinateLinearMap: the coordinate field as an operator on its generating vector.
• contDiffAt_mulInvariantCoordinateLinearMap_one: this operator is C^n at the identity coordinate.
• hasStrictFDerivAt_mulInvariantCoordinateVectorField_zero_one: the linearization of the parameterized coordinate field at zero and the identity is projection onto the parameter.
• exists_lipschitzOn_local_mulInvariantCoordinateFlow: a local solution family on a uniform closed neighborhood of the zero vector and the identity coordinate, jointly continuous and uniformly Lipschitz in its initial state.
• exists_eventually_hasDerivAt_mulInvariantCoordinateFlow: a neighborhood form of the local solution family whose values remain inside the identity chart.
• exists_local_coordinate_representation_mulInvariantIntegralCurve: the local solution family solves the coordinate ODE and represents the canonical integral curves uniformly for all small generators.
• continuousAt_mulInvariantExp_modelSpace_zero: the tangent-space exponential is continuous at zero in model-space coordinates.

References

• Lie groups and the Lie algebra correspondence roadmap, Deliverable A, Layer 0, "The exponential map".
• Winston Yin's Mathlib proof of exists_isMIntegralCurveAt_of_contMDiffAt_boundaryless, whose chart calculation is exposed by IsMIntegralCurveAt.of_extChartAt_symm and invoked below.

noncomputable def mulInvariantCoordinateVectorField {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] [IsManifold I 1 G] (p : E × E) : E

The left-invariant vector field, expressed in the identity chart and parameterized by its generating tangent vector in the model space.

theorem mulInvariantCoordinateVectorField_apply {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] [IsManifold I 1 G] (v y : E) : mulInvariantCoordinateVectorField (v, y) = (tangentCoordChange I (↑(extChartAt I 1).symm y) 1 (↑(extChartAt I 1).symm y)) (mulInvariantVectorField v (↑(extChartAt I 1).symm y))

The parameterized coordinate field is the invariant vector field transported through the identity chart.

@[simp]

theorem mulInvariantCoordinateVectorField_add {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] [IsManifold I 1 G] (v w y : E) : mulInvariantCoordinateVectorField (v + w, y) = mulInvariantCoordinateVectorField (v, y) + mulInvariantCoordinateVectorField (w, y)

The invariant coordinate field is additive in its generating vector.

@[simp]

theorem mulInvariantCoordinateVectorField_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] [IsManifold I 1 G] (c : ℝ) (v y : E) : mulInvariantCoordinateVectorField (c • v, y) = c • mulInvariantCoordinateVectorField (v, y)

The invariant coordinate field respects scalar multiplication in its generating vector.

@[simp]

theorem mulInvariantCoordinateVectorField_one {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] [IsManifold I 1 G] (v : E) : mulInvariantCoordinateVectorField (v, ↑I (↑(chartAt H 1) 1)) = v

At the identity coordinate, the parameterized invariant field equals its generator.

@[simp]

theorem mulInvariantCoordinateVectorField_zero {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] [IsManifold I 1 G] (y : E) : mulInvariantCoordinateVectorField (0, y) = 0

The invariant coordinate field vanishes when its generating vector vanishes.

theorem contDiffAt_mulInvariantCoordinateVectorField {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] (v : E) {n : WithTop ℕ∞} [ContMDiffMul I (n + 1) G] (h1 : I.IsInteriorPoint 1) : have x := ⋯; ContDiffAt ℝ n mulInvariantCoordinateVectorField (v, ↑(extChartAt I 1) 1)

The coordinate expression of the parameterized left-invariant vector field is C^n at every generating vector over the identity coordinate when multiplication is C^(n + 1).

noncomputable def mulInvariantCoordinateLinearMap {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] [IsManifold I 1 G] (y : E) : E →L[ℝ] E

At a fixed identity-chart coordinate, the invariant coordinate field as a continuous linear map of its generating model vector.

@[simp]

theorem mulInvariantCoordinateLinearMap_apply {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] [IsManifold I 1 G] (y v : E) : (mulInvariantCoordinateLinearMap y) v = mulInvariantCoordinateVectorField (v, y)

Applying the coordinate-field linear map recovers the parameterized coordinate vector field.

@[simp]

theorem mulInvariantCoordinateLinearMap_one {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] [IsManifold I 1 G] : mulInvariantCoordinateLinearMap (↑I (↑(chartAt H 1) 1)) = ContinuousLinearMap.id ℝ E

At the identity coordinate, the coordinate-field linear map is the identity operator.

theorem contDiffAt_mulInvariantCoordinateLinearMap_one {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] {n : WithTop ℕ∞} [FiniteDimensional ℝ E] [ContMDiffMul I (n + 1) G] (h1 : I.IsInteriorPoint 1) : have x := ⋯; ContDiffAt ℝ n mulInvariantCoordinateLinearMap (↑(extChartAt I 1) 1)

In finite dimensions, the coordinate-field linear map is C^n at the identity coordinate.

theorem hasStrictFDerivAt_mulInvariantCoordinateVectorField_zero_one {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] [ContMDiffMul I (1 + 1) G] (h1 : I.IsInteriorPoint 1) : have x := ⋯; HasStrictFDerivAt mulInvariantCoordinateVectorField (ContinuousLinearMap.fst ℝ E E) (0, ↑(extChartAt I 1) 1)

At the zero generating vector over the identity coordinate, the parameterized coordinate vector field has strict derivative equal to projection onto the generating-vector coordinate.

theorem exists_lipschitzOn_local_mulInvariantCoordinateFlow {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] [CompleteSpace E] [ContMDiffMul I (1 + 1) G] (h1 : I.IsInteriorPoint 1) : have x := ⋯; ∃ (α : (E × E) × ℝ → E × E) (δ : ℝ) (r : NNReal) (L : NNReal), 0 < δ ∧ 0 < r ∧ ContinuousOn α (Metric.closedBall (0, ↑(extChartAt I 1) 1) ↑r ×ˢ Set.Icc (-δ) δ) ∧ (∀ t ∈ Set.Icc (-δ) δ, LipschitzOnWith L (fun (x : E × E) => α (x, t)) (Metric.closedBall (0, ↑(extChartAt I 1) 1) ↑r)) ∧ ∀ x_1 ∈ Metric.closedBall (0, ↑(extChartAt I 1) 1) ↑r, α (x_1, 0) = x_1 ∧ (∀ t ∈ Set.Icc (-δ) δ, HasDerivWithinAt (fun (s : ℝ) => α (x_1, s)) (0, mulInvariantCoordinateVectorField (α (x_1, t))) (Set.Icc (-δ) δ) t) ∧ ∀ t ∈ Set.Icc (-δ) δ, (α (x_1, t)).1 = x_1.1

Near the zero tangent vector and the identity coordinate, the parameterized invariant ODE has a single solution family that is continuous jointly in its initial condition and time and uniformly Lipschitz in its initial state. The tangent-vector coordinate is frozen by the ODE; the second coordinate follows the invariant vector field.

theorem exists_eventually_hasDerivAt_mulInvariantCoordinateFlow {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] [CompleteSpace E] [ContMDiffMul I (1 + 1) G] (h1 : I.IsInteriorPoint 1) : have x := ⋯; ∃ (α : (E × E) × ℝ → E × E), (∀ᶠ (xt : (E × E) × ℝ) in nhds ((0, ↑(extChartAt I 1) 1), 0), ContinuousAt α xt) ∧ ∀ᶠ (xt : (E × E) × ℝ) in nhds ((0, ↑(extChartAt I 1) 1), 0), HasDerivAt (fun (t : ℝ) => α (xt.1, t)) (0, mulInvariantCoordinateVectorField (α xt)) xt.2 ∧ α (xt.1, 0) = xt.1 ∧ (α xt).1 = xt.1.1 ∧ (α xt).2 ∈ interior (extChartAt I 1).target

There is a coordinate solution family near the zero tangent vector and time zero which is continuous at the center, solves the parameterized invariant ODE with an ordinary derivative, freezes the tangent-vector parameter, and remains in the target of the identity chart.

theorem exists_local_coordinate_representation_mulInvariantIntegralCurve {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] [CompleteSpace E] [LieGroup I (minSmoothness ℝ 3) G] [T2Space G] [BoundarylessManifold I G] : ∃ (α : (E × E) × ℝ → E × E) (U : Set E) (δ : ℝ), U ∈ nhds 0 ∧ 0 < δ ∧ (∀ v ∈ U, ∀ t ∈ Set.Ioo (-δ) δ, ContinuousAt α ((v, ↑(extChartAt I 1) 1), t) ∧ HasDerivAt (fun (s : ℝ) => α ((v, ↑(extChartAt I 1) 1), s)) (0, mulInvariantCoordinateVectorField (α ((v, ↑(extChartAt I 1) 1), t))) t ∧ α ((v, ↑(extChartAt I 1) 1), 0) = (v, ↑(extChartAt I 1) 1) ∧ (α ((v, ↑(extChartAt I 1) 1), t)).1 = v ∧ (α ((v, ↑(extChartAt I 1) 1), t)).2 ∈ interior (extChartAt I 1).target) ∧ ∀ v ∈ U, Set.EqOn (fun (t : ℝ) => ↑(extChartAt I 1).symm (α ((v, ↑(extChartAt I 1) 1), t)).2) (mulInvariantIntegralCurve v 1) (Set.Ioo (-δ) δ)

A single coordinate solution family solves the invariant coordinate ODE and represents the canonical invariant integral curves for every sufficiently small generating vector and every sufficiently small time. This bridges Picard--Lindelöf's parameterized model-space solutions to the canonical manifold-valued curves used to define lieExp.

theorem continuousAt_mulInvariantExp_modelSpace_zero {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] [CompleteSpace E] [LieGroup I (minSmoothness ℝ 3) G] [T2Space G] [BoundarylessManifold I G] : ContinuousAt (fun (v : E) => mulInvariantExp v) 0

The tangent-space exponential is continuous at zero when its domain uses the canonical model-space identification and its codomain remains the Lie group G.