CartanFactorCharts.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Actual factor-chart continuity and the exponential Cartan action

theorem OAI.PolycyclicRecognition.continuous_model_exp_coordinates line 17

Source documentation

The published nilpotent exponential chart makes every identified linear coordinate chart continuous.

theorem continuous_model_exp_coordinates
    {E N L : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [FiniteDimensional ℝ E] [TopologicalSpace N] [ChartedSpace E N] [Group N]
    [LieGroup (𝓘(ℝ, E)) ⊤ N] [T2Space N] [SimplyConnectedSpace N]
    [MeasurableSpace N] [BorelSpace N] [LieRing L] [LieAlgebra ℝ L]
    (haar : NilpotentExponentialHaarInput E N)
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) N → N) (hExp : IsGroupExponential Exp)
    (e : L ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, E)) N)
    (hnil : LieRing.IsNilpotent (GroupLieAlgebra (𝓘(ℝ, E)) N))
    {n : ℕ} (b : Basis (Fin n) ℝ L) :
    Continuous (fun z => Exp (e (b.equivFun.symm z))) := by
…

Mentions: OAI.PolycyclicRecognition.NilpotentExponentialHaarInput

theorem OAI.PolycyclicRecognition.cartan_action_exp_of_published_realization line 48
Source documentation
The exact exponential action needed by the chart normalization formula follows from the published faithful realization, with no new action input.
```
theorem cartan_action_exp_of_published_realization
    (hExpG : IsGroupExponential ExpG)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…
```
Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput