GeneratorOrbit.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Spanning by conjugated generator directions

Products of adjoint exponentials applied to a Lie-generating family span the whole algebra. This proves the linear nondegeneracy needed to construct a submersive generator product scheme; it does not assume controllability or a volume estimate.

def OAI.PolycyclicRecognition.continuousAd line 32
Source documentation
The adjoint operator, with its finite-dimensional continuous structure.
```
def continuousAd (x : L) : L →L[ℝ] L := Module.End.toContinuousLinearMap (𝕜 := ℝ) L (LieModule.toEnd ℝ L L x)
```
theorem OAI.PolycyclicRecognition.continuousAd_apply line 34
def OAI.PolycyclicRecognition.generatorAdjointWord line 37
Source documentation
A finite product of actual operator exponentials of generator adjoints.
```
def generatorAdjointWord (X : I → L) (w : List (I × ℝ)) : L →L[ℝ] L :=
…
```
theorem OAI.PolycyclicRecognition.generatorAdjointWord_nil line 40
theorem OAI.PolycyclicRecognition.generatorAdjointWord_cons line 43
def OAI.PolycyclicRecognition.generatorOrbitSpan line 49
Source documentation
The linear span of all conjugated generator directions.
```
def generatorOrbitSpan (X : I → L) : Submodule ℝ L :=
…
```
theorem OAI.PolycyclicRecognition.generator_mem_orbitSpan line 53
theorem OAI.PolycyclicRecognition.exp_ad_mem_orbitSpan line 58
Source documentation
Each adjoint exponential preserves this span by prefixing a word.
```
theorem exp_ad_mem_orbitSpan (X : I → L) (i : I) (t : ℝ) {v : L}
    (hv : v ∈ generatorOrbitSpan X) :
    NormedSpace.exp (t • continuousAd (X i)) v ∈ generatorOrbitSpan X := by
…
```
Mentions: OAI.PolycyclicRecognition.generatorOrbitSpan, OAI.PolycyclicRecognition.continuousAd
theorem OAI.PolycyclicRecognition.hasDerivAt_exp_ad_apply line 71
Source documentation
Differentiating the genuine operator exponential recovers the adjoint.
```
theorem hasDerivAt_exp_ad_apply (x v : L) :
    HasDerivAt (fun t : ℝ => NormedSpace.exp (t • continuousAd x) v) ⁅x, v⁆ 0 := by
…
```
Mentions: OAI.PolycyclicRecognition.continuousAd

theorem OAI.PolycyclicRecognition.derivative_mem_submodule line 78

Source documentation

A derivative of a curve in a closed linear subspace stays in that subspace.

theorem derivative_mem_submodule {f : ℝ → L} {v : L} {t : ℝ}
    (hf : HasDerivAt f v t) (U : Submodule ℝ L) (hU : ∀ s, f s ∈ U) : v ∈ U := by
…

theorem OAI.PolycyclicRecognition.ad_mem_orbitSpan line 90
Source documentation
Invariance under generator exponentials implies infinitesimal invariance.
```
theorem ad_mem_orbitSpan (X : I → L) (i : I) {v : L}
    (hv : v ∈ generatorOrbitSpan X) : ⁅X i, v⁆ ∈ generatorOrbitSpan X :=
…
```
Mentions: OAI.PolycyclicRecognition.generatorOrbitSpan
def OAI.PolycyclicRecognition.submoduleAdjointStabilizer line 97
Source documentation
The elements whose adjoints preserve a fixed linear subspace form a Lie subalgebra, by the Jacobi identity.
```
def submoduleAdjointStabilizer (U : Submodule ℝ L) : LieSubalgebra ℝ L where
…
```
theorem OAI.PolycyclicRecognition.generatorOrbitSpan_eq_top line 113
Source documentation
The conjugated generator directions span the entire generated Lie algebra. No nilpotence assumption is needed for this nondegeneracy step.
```
theorem generatorOrbitSpan_eq_top (X : I → L)
    (hX : LieSubalgebra.lieSpan ℝ L (Set.range X) = ⊤) :
    generatorOrbitSpan X = ⊤ := by
…
```
Mentions: OAI.PolycyclicRecognition.generatorOrbitSpan

theorem OAI.PolycyclicRecognition.exists_generatorOrbit_basis line 138

Source documentation

Choose finitely many actual conjugated generator directions as a basis. These are the differential columns in a conjugated generator scheme.

theorem exists_generatorOrbit_basis (X : I → L)
    (hX : LieSubalgebra.lieSpan ℝ L (Set.range X) = ⊤) :
    ∃ (b : Basis (Fin (finrank ℝ L)) ℝ L)
      (w : Fin (finrank ℝ L) → List (I × ℝ)) (i : Fin (finrank ℝ L) → I),
      ∀ k, generatorAdjointWord X (w k) (X (i k)) = b k := by
…

Mentions: OAI.PolycyclicRecognition.generatorAdjointWord