CommonDynkinFormula.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A common BCH formula for two nilpotent Lie groups

Apply the published finite Dynkin identity once to the product group, then project to each factor. The projections preserve the actual tangent bracket.

def OAI.PolycyclicRecognition.exponentialProductLieModel line 30
Source documentation
The product is packaged solely to instantiate the existing published input. Its measurable structure is the Borel structure of the product.
```
def exponentialProductLieModel
    (cG : GroupLieAlgebra (𝓘(ℝ, E)) G ≃ₜ G)
    (cH : GroupLieAlgebra (𝓘(ℝ, F)) H ≃ₜ H) :
    NilpotentLieModel (GroupLieAlgebra (𝓘(ℝ, E × F)) (G × H)) := by
…
```
Mentions: OAI.PolycyclicRecognition.NilpotentLieModel
theorem OAI.PolycyclicRecognition.exists_common_dynkin_formula line 42