BilinearGeneratorOrbit.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Generator adjoint orbits in a fixed coordinate norm

This is the coordinate version of the spanning argument. Its exponential operators use the fixed norm on the parameter space, so they vary continuously with the bilinear bracket, including at limiting laws.

def OAI.PolycyclicRecognition.bilinearAdjointWord line 22
def OAI.PolycyclicRecognition.bilinearOrbitSpan line 26
theorem OAI.PolycyclicRecognition.bilinear_generator_mem_orbitSpan line 31
theorem OAI.PolycyclicRecognition.bilinear_exp_mem_orbitSpan line 37
theorem OAI.PolycyclicRecognition.bilinear_ad_mem_orbitSpan line 52
Source documentation
Differentiating the fixed-norm adjoint exponential stays in its closed orbit span.
```
theorem bilinear_ad_mem_orbitSpan (B : V →L[ℝ] V →L[ℝ] V)
    (X : I → V) (i : I) {v : V} (hv : v ∈ bilinearOrbitSpan B X) :
    B (X i) v ∈ bilinearOrbitSpan B X := by
…
```
Mentions: OAI.PolycyclicRecognition.bilinearOrbitSpan
theorem OAI.PolycyclicRecognition.bilinearOrbitSpan_eq_top line 69
Source documentation
Exact word-basis normalization implies spanning by the coordinate adjoint orbits, for every law in the compact family.
```
theorem bilinearOrbitSpan_eq_top {J : Type*}
    (B : V →L[ℝ] V →L[ℝ] V) (hB : IsLieBracket B)
    (X : I → V) (b : Basis J ℝ V) (w : J → FreeMagma I)
    (hw : ∀ j, evalBilinearWord B X (w j) = b j) :
    bilinearOrbitSpan B X = ⊤ := by
…
```
Mentions: OAI.PolycyclicRecognition.IsLieBracket, OAI.PolycyclicRecognition.evalBilinearWord, OAI.PolycyclicRecognition.bilinearOrbitSpan

theorem OAI.PolycyclicRecognition.exists_bilinearOrbit_basis line 99

Source documentation

A finite basis of fixed-norm adjoint words can be selected at each limiting law. This is the nondegeneracy used by the uniform-chart argument.

theorem exists_bilinearOrbit_basis {J : Type*}
    (B : V →L[ℝ] V →L[ℝ] V) (hB : IsLieBracket B)
    (X : I → V) (b₀ : Basis J ℝ V) (w₀ : J → FreeMagma I)
    (hw₀ : ∀ j, evalBilinearWord B X (w₀ j) = b₀ j) :
    ∃ (b : Basis (Fin (finrank ℝ V)) ℝ V)
      (w : Fin (finrank ℝ V) → List (I × ℝ)) (i : Fin (finrank ℝ V) → I),
      ∀ k, bilinearAdjointWord B X (w k) (X (i k)) = b k := by
…

Mentions: OAI.PolycyclicRecognition.IsLieBracket, OAI.PolycyclicRecognition.evalBilinearWord, OAI.PolycyclicRecognition.bilinearAdjointWord