NilpotentPublishedInputs.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The nilpotent published-input family used by the Cartan construction

The finite BCH expansion follows Baudoin (2004), Appendix B.5--B.6. The intrinsic adjoint calculation and integration into arbitrary Lie groups give model existence, global coordinates, integration, and exponential Haar compatibility.

structure OAI.PolycyclicRecognition.NilpotentPublishedInputs line 25
theorem OAI.PolycyclicRecognition.NilpotentPublishedInputs.existsModel line 30
Source documentation
Codimension-one induction constructs the analytic simply connected model.
```
theorem NilpotentPublishedInputs.existsModel (_h : NilpotentPublishedInputs)
    (L : Type) [LieRing L] [LieAlgebra ℝ L] [FiniteDimensional ℝ L] :
    NilpotentLieExistenceInput L :=
…
```
Mentions: OAI.PolycyclicRecognition.NilpotentPublishedInputs, OAI.PolycyclicRecognition.NilpotentLieExistenceInput
theorem OAI.PolycyclicRecognition.NilpotentPublishedInputs.coordinates line 36
Source documentation
Finite BCH and simple connectedness give the global exponential chart.
```
theorem NilpotentPublishedInputs.coordinates (h : NilpotentPublishedInputs)
    (L : Type) [LieRing L] [LieAlgebra ℝ L] [FiniteDimensional ℝ L]
    (N : NilpotentLieModel L) : NilpotentGlobalExponentialChartInput N.modelSpace N.carrier :=
…
```
Mentions: OAI.PolycyclicRecognition.NilpotentPublishedInputs, OAI.PolycyclicRecognition.NilpotentLieModel, OAI.PolycyclicRecognition.NilpotentGlobalExponentialChartInput
theorem OAI.PolycyclicRecognition.NilpotentPublishedInputs.haar line 43
Source documentation
Global integral curves give the exponential, and the BCH Jacobian gives the Haar compatibility of every exponential basis chart.
```
theorem NilpotentPublishedInputs.haar (h : NilpotentPublishedInputs)
    (L : Type) [LieRing L] [LieAlgebra ℝ L] [FiniteDimensional ℝ L]
    (N : NilpotentLieModel L) : NilpotentExponentialHaarInput N.modelSpace N.carrier :=
…
```
Mentions: OAI.PolycyclicRecognition.NilpotentPublishedInputs, OAI.PolycyclicRecognition.NilpotentLieModel, OAI.PolycyclicRecognition.NilpotentExponentialHaarInput
theorem OAI.PolycyclicRecognition.NilpotentPublishedInputs.integrate line 50
Source documentation
The nilpotent-target specialization is constructed from exponential coordinates and the common BCH identity on the product group.
```
theorem NilpotentPublishedInputs.integrate (h : NilpotentPublishedInputs)
    (L K : Type) [LieRing L] [LieAlgebra ℝ L] [FiniteDimensional ℝ L]
    [LieRing K] [LieAlgebra ℝ K] [FiniteDimensional ℝ K] [LieRing.IsNilpotent K]
    (N : NilpotentLieModel L) (Q : NilpotentLieModel K) :
    NilpotentLieIntegrationInput (EN := N.modelSpace) (N := N.carrier)
…
```
Mentions: OAI.PolycyclicRecognition.NilpotentPublishedInputs, OAI.PolycyclicRecognition.NilpotentLieModel, OAI.PolycyclicRecognition.NilpotentLieIntegrationInput
theorem OAI.PolycyclicRecognition.NilpotentPublishedInputs.polar line 67
Source documentation
The six inputs for each actual cone are specializations of the cited nilpotent theorems. Cone geometry itself is not assumed.
```
theorem NilpotentPublishedInputs.polar (h : NilpotentPublishedInputs)
    (M : CartanWordModel H) {Exp : GroupLieAlgebra (𝓘(ℝ, EG)) G → G}
    (F : CartanFactorModel H Exp) (C : Set (H →ₗ[ℝ] ℝ)) :
    M.PolarConeModelInputs F C := by
…
```
Mentions: OAI.PolycyclicRecognition.NilpotentPublishedInputs, OAI.PolycyclicRecognition.CartanWordModel, OAI.PolycyclicRecognition.CartanFactorModel