CartanSemidirectWords.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Controlled words in the actual semidirect product

Nilpotent Cartan increments give polynomial bounds on every Cartan prefix. The exact semidirect-product formula then reduces its nilpotent coordinate to the controlled product estimate. No polynomial bound on prefixes is left as an assumption of this theorem.

theorem OAI.PolycyclicRecognition.CartanWordModel.action_eq_adjoint_of_representation line 49

Source documentation

The required semidirect action identity follows from compatible exponentials in an ambient faithful representation.

theorem action_eq_adjoint_of_representation
    (j : L →ₗ⁅ℝ⁆ A) (ρ : G →* Aˣ) (hρ : Function.Injective ρ)
    (ιN : N →* G) (hιN : Function.Injective ιN) (ιD : D →* G)
    (hconj : ∀ d g, ιN (φ d g) = ιD d * ιN g * (ιD d)⁻¹)
    (hN : ∀ x : cartanRootIdeal H, ρ (ιN (ExpN (eN x))) = algebraExpUnit (j x))
    (hD : ∀ h : H, ρ (ιD (ExpD (eD h))) = algebraExpUnit (j h)) (d : D) :
    φ d = M.adjointGroupAutomorphism T eN ExpN hExpN hbijN dynkinN
      (cartanLog H eD ExpD hbijD d) := by
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.algebraExpUnit, OAI.PolycyclicRecognition.cartanLog

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_semidirect_word_bound line 70

Source documentation

Bounded increments and containment of the actual prefix heights imply a polynomial bound for the nilpotent coordinate of the full word.

theorem exists_semidirect_word_bound
    (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
    (hφ : ∀ d, φ d = M.adjointGroupAutomorphism T eN ExpN hExpN hbijN dynkinN
      (cartanLog H eD ExpD hbijD d))
    {RN RD : ℝ} (hRN : 0 ≤ RN) (hRD : 0 ≤ RD) :
    ∃ (C : ℝ) (q : ℕ), 0 ≤ C ∧ ∀ {E : Set W}, IsCompact E → E.Nonempty →
      ∀ β : M.Bases,
      IsMaximizingColumnBasis (wordListCoordinates M.letter M.wordList b₀)
        (M.boxCost T hunimod eW E) β.val →
      ∀ (γ : M.Bases) (r : ℝ), 0 ≤ r → ∀ (m : ℕ) (u : ℕ → N) (v : ℕ → D),
      (∀ i < m, u i ∈ exponentialCoordinateBox (ExpN ∘ eN)
        (WordBasisSelections.basis M.letter M.wordList γ) RN) →
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.cartanLog, OAI.PolycyclicRecognition.IsMaximizingColumnBasis, OAI.PolycyclicRecognition.wordListCoordinates, OAI.PolycyclicRecognition.exponentialCoordinateBox, OAI.PolycyclicRecognition.WordBasisSelections.basis