SequenceCartanPrefixes.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform Cartan logarithms for a fixed finite number of transitions

theorem OAI.PolycyclicRecognition.exists_sequence_cartan_prefix_bound line 23

Source documentation

Polynomial word growth is uniform for all prefixes of a fixed finite tuple, even when the allowed single-transition radius varies subexponentially.

theorem exists_sequence_cartan_prefix_bound
    (hExpD : IsGroupExponential ExpD) (dynkinD : NilpotentDynkinExpansionInput ED D)
    (h : ℕ) (scale R : ℕ → ℝ) (hs : Tendsto scale atTop atTop)
    (hR0 : ∀ n, 0 ≤ R n) (hR : HasSubexponentialUpperBoundSeq scale R) :
    ∃ S : ℕ → ℝ, (∀ n, 0 ≤ S n) ∧ HasSubexponentialUpperBoundSeq scale S ∧
      ∀ n (u : ℕ → D),
        (∀ j < h, ‖(finBasis ℝ H).equivFun (cartanLog H eD ExpD hbijD (u j))‖ ≤ R n) →
        ∀ m ≤ h, ‖(finBasis ℝ H).equivFun
          (cartanLog H eD ExpD hbijD (wordPrefix u m))‖ ≤ S n := by
…

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