CompactLieLaws.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Compact families of normalized Lie laws

Bounded brackets and generators satisfying fixed word-basis identities form a compact parameter set. Limits retain the Lie identities and the exact word normalizations, so bracket generation cannot disappear in a limit.

def OAI.PolycyclicRecognition.lieRingOfBilinear line 24
Source documentation
A bilinear bracket satisfying alternation and Jacobi gives the ordinary Lie ring structure on the existing additive group.
```
@[instance_reducible] def lieRingOfBilinear (B : V →L[ℝ] V →L[ℝ] V) (h : IsLieBracket B) : LieRing V where
…
```
Mentions: OAI.PolycyclicRecognition.IsLieBracket
def OAI.PolycyclicRecognition.lieAlgebraOfBilinear line 33
Source documentation
The bracket is compatible with the original real vector-space structure.
```
@[instance_reducible] def lieAlgebraOfBilinear (B : V →L[ℝ] V →L[ℝ] V) (h : IsLieBracket B) :
    @LieAlgebra ℝ V _ (lieRingOfBilinear B h) := by
…
```
Mentions: OAI.PolycyclicRecognition.IsLieBracket, OAI.PolycyclicRecognition.lieRingOfBilinear
def OAI.PolycyclicRecognition.normalizedLieParameters line 42
Source documentation
Parameter data for a fixed normalization by bracket words.
```
def normalizedLieParameters (w : J → FreeMagma I) (b : J → V) (C : ℝ) :
    Set ((V →L[ℝ] V →L[ℝ] V) × (I → V)) :=
…
```
theorem OAI.PolycyclicRecognition.isCompact_normalizedLieParameters line 49
Source documentation
The exact word identities are closed, while the coefficient and letter bounds give a compact ambient set.
```
theorem isCompact_normalizedLieParameters
    (w : J → FreeMagma I) (b : J → V) (C : ℝ) :
    IsCompact (normalizedLieParameters w b C) := by
…
```
Mentions: OAI.PolycyclicRecognition.normalizedLieParameters