CoordinateLieBrackets.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The actual Lie law in a chosen basis

Transport the original bracket to Euclidean coordinates, retaining its exact word identities. A bound on basis structure constants gives a bound in the finite-dimensional parameter space used for normalized-law compactness.

def OAI.PolycyclicRecognition.basisBracketLinear line 23
Source documentation
Coordinate transport of the bracket, initially as a bilinear map.
```
def basisBracketLinear : (Fin n → ℝ) →ₗ[ℝ] (Fin n → ℝ) →ₗ[ℝ] (Fin n → ℝ) where
…
```
def OAI.PolycyclicRecognition.basisBracket line 45
Source documentation
The same coordinate bracket in the normed space of continuous bilinear maps.
```
def basisBracket : (Fin n → ℝ) →L[ℝ] (Fin n → ℝ) →L[ℝ] (Fin n → ℝ) :=
…
```
theorem OAI.PolycyclicRecognition.basisBracket_apply line 50
theorem OAI.PolycyclicRecognition.isLieBracket_basisBracket line 55
Source documentation
The transported operation is a genuine Lie bracket, not only a bounded bilinear operation.
```
theorem isLieBracket_basisBracket : IsLieBracket (basisBracket b) := by
…
```
Mentions: OAI.PolycyclicRecognition.IsLieBracket, OAI.PolycyclicRecognition.basisBracket
theorem OAI.PolycyclicRecognition.evalBilinearWord_basisBracket line 64
Source documentation
Word evaluation commutes exactly with the coordinate transport.
```
theorem evalBilinearWord_basisBracket {I : Type*} (X : I → L) (w : FreeMagma I) :
    evalBilinearWord (basisBracket b) (fun i => b.equivFun (X i)) w =
      b.equivFun (evalBracketWord X w) := by
…
```
Mentions: OAI.PolycyclicRecognition.evalBilinearWord, OAI.PolycyclicRecognition.basisBracket, OAI.PolycyclicRecognition.evalBracketWord
theorem OAI.PolycyclicRecognition.norm_basisBracket_le line 76
Source documentation
The structure-constant estimate controls the norm of the actual law in the fixed coordinate parameter space.
```
theorem norm_basisBracket_le {C : ℝ} (hC : 0 ≤ C)
    (hb : ∀ i j k, |b.repr ⁅b i, b j⁆ k| ≤ C) :
    ‖basisBracket b‖ ≤ (n : ℝ) ^ 2 * C := by
…
```
Mentions: OAI.PolycyclicRecognition.basisBracket