CartanWordLogarithms.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Cartan logarithms of bounded words

The Cartan group is nilpotent. The finite Dynkin identity therefore gives a polynomial bound on the logarithm of every prefix of a bounded word. We also record the exact semidirect-product word formula used to apply the controlled Cartan estimates to such prefixes.

def OAI.PolycyclicRecognition.wordPrefix line 23
Source documentation
Ordered product of the first m letters of a word.
```
def wordPrefix {G : Type*} [Monoid G] (u : ℕ → G) (m : ℕ) : G :=
…
```
theorem OAI.PolycyclicRecognition.wordPrefix_zero line 26
theorem OAI.PolycyclicRecognition.wordPrefix_succ line 29
theorem OAI.PolycyclicRecognition.semidirect_wordPrefix_right line 35

theorem OAI.PolycyclicRecognition.semidirect_wordPrefix_left line 45

Source documentation

The nilpotent component of a semidirect word is the ordered product of the nilpotent increments acted on by the actual Cartan prefixes.

theorem semidirect_wordPrefix_left {N D : Type*} [Group N] [Group D]
    (φ : D →* MulAut N) (u : ℕ → N) (v : ℕ → D) (m : ℕ) :
    (wordPrefix (fun i => (⟨u i, v i⟩ : N ⋊[φ] D)) m).left =
      wordPrefix (fun i => φ (wordPrefix v i) (u i)) m := by
…

Mentions: OAI.PolycyclicRecognition.wordPrefix

def OAI.PolycyclicRecognition.cartanLog line 64
Source documentation
The Cartan logarithm in the actual nilpotent exponential coordinates.
```
def cartanLog (d : D) : H := eD.symm ((Equiv.ofBijective ExpD hbijD).symm d)
…
```
theorem OAI.PolycyclicRecognition.cartanLog_exp line 67
theorem OAI.PolycyclicRecognition.exp_cartanLog line 74

theorem OAI.PolycyclicRecognition.exists_cartan_word_log_bound line 81

Source documentation

Bounded Cartan increments have polynomial logarithmic coordinates. The nilpotence bound comes from the Cartan subalgebra itself.

theorem exists_cartan_word_log_bound
    (hExpD : IsGroupExponential ExpD) (dynkinD : NilpotentDynkinExpansionInput ED D)
    {R : ℝ} (hR : 0 ≤ R) :
    ∃ (A : ℝ) (c : ℕ), 0 ≤ A ∧ ∀ (u : ℕ → D) (m : ℕ),
      (∀ i < m, u i ∈ exponentialCoordinateBox (ExpD ∘ eD) (finBasis ℝ H) R) →
      ‖(finBasis ℝ H).equivFun (cartanLog H eD ExpD hbijD (wordPrefix u m))‖ ≤
        A * (1 + (m : ℝ)) ^ c := by
…

Mentions: OAI.PolycyclicRecognition.NilpotentDynkinExpansionInput, OAI.PolycyclicRecognition.exponentialCoordinateBox, OAI.PolycyclicRecognition.cartanLog, OAI.PolycyclicRecognition.wordPrefix