GeneratorSchemes.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Finite generator schemes with locally open endpoint maps

A conjugated-generator basis gives a single finite scheme, with fixed conjugating words, whose endpoint map covers a neighborhood of the identity. The logarithm of that map has the identity-rank differential proved from BCH.

def OAI.PolycyclicRecognition.inverseGeneratorWord line 29
Source documentation
Reverse a generator word and negate its one-parameter amplitudes.
```
def inverseGeneratorWord (w : List (I × ℝ)) : List (I × ℝ) :=
…
```
theorem OAI.PolycyclicRecognition.generatorGroupWord_append line 34
theorem OAI.PolycyclicRecognition.generatorGroupWord_inverse line 39
def OAI.PolycyclicRecognition.generatorSchemeWord line 54
Source documentation
Fixed conjugating words with one variable generator inserted in each.
```
def generatorSchemeWord {n : ℕ} (w : Fin n → List (I × ℝ)) (i : Fin n → I)
    (t : Fin n → ℝ) : List (I × ℝ) :=
…
```
theorem OAI.PolycyclicRecognition.length_generatorSchemeWord line 59
Source documentation
The word length is fixed even though the inserted amplitudes vary.
```
theorem length_generatorSchemeWord {n : ℕ} (w : Fin n → List (I × ℝ)) (i : Fin n → I)
    (t : Fin n → ℝ) :
    (generatorSchemeWord w i t).length = ∑ k, (2 * (w k).length + 1) := by
…
```
Mentions: OAI.PolycyclicRecognition.generatorSchemeWord

theorem OAI.PolycyclicRecognition.generatorScheme_endpoint line 70

Source documentation

Endpoint of the expanded scheme is exactly the product in the chosen basis directions.

theorem generatorScheme_endpoint {n : ℕ}
    (b : Basis (Fin n) ℝ L) (w : Fin n → List (I × ℝ)) (i : Fin n → I)
    (hneg : ∀ x, Exp (-x) = (Exp x)⁻¹)
    (hb : ∀ k (s : ℝ), Exp (s • b k) =
      generatorGroupWord X Exp (w k) * Exp (s • X (i k)) *
        (generatorGroupWord X Exp (w k))⁻¹)
    (t : Fin n → ℝ) :
    generatorGroupWord X Exp (generatorSchemeWord w i t) = basisExponentialProduct Exp b t := by
…

Mentions: OAI.PolycyclicRecognition.generatorGroupWord, OAI.PolycyclicRecognition.generatorSchemeWord, OAI.PolycyclicRecognition.basisExponentialProduct

theorem OAI.PolycyclicRecognition.exists_local_generator_scheme line 96

Source documentation

The actual finite scheme and a neighborhood covered with bounded variable amplitudes. All the hypotheses are algebraic representation/BCH identities; local surjectivity is proved, not assumed.

theorem exists_local_generator_scheme
    (hX : LieSubalgebra.lieSpan ℝ L (Set.range X) = ⊤)
    (hExp : Function.Bijective Exp) (hzero : Exp 0 = 1)
    (hneg : ∀ x, Exp (-x) = (Exp x)⁻¹)
    (j : L →ₗ⁅ℝ⁆ A) (ρ : G →* Aˣ) (hρ : Function.Injective ρ)
    (hmatch : ∀ x, ρ (Exp x) = algebraExpUnit (j x))
    {c : ℕ} (coeff : DynkinCoefficients c (finrank ℝ L))
    (hprod : ∀ Z : Fin (finrank ℝ L) → L,
      (List.ofFn (fun k => Exp (Z k))).prod = Exp (finiteDynkinPolynomial coeff Z)) :
    ∃ (w : Fin (finrank ℝ L) → List (I × ℝ)) (i : Fin (finrank ℝ L) → I)
      (ε : ℝ), 0 < ε ∧ ∀ v : L, ‖v‖ < ε →
      ∃ t : Fin (finrank ℝ L) → ℝ, ‖t‖ < 1 ∧
…

Mentions: OAI.PolycyclicRecognition.algebraExpUnit, OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.finiteDynkinPolynomial