CartanCompactWords.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Compact increments in the Cartan word model

Compact sets of increments have bounded logarithms in the published global nilpotent exponential charts. This removes the coordinate-radius assumptions from the semidirect word estimate and leaves ordinary compact step data.

theorem OAI.PolycyclicRecognition.exists_compact_exponential_coordinate_bound line 21

Source documentation

A compact subset has bounded coordinates in any global exponential chart, without choosing a norm on the abstract Lie-algebra model.

theorem exists_compact_exponential_coordinate_bound
    {L : Type*} [LieRing L] [LieAlgebra ℝ L]
    {E G : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    [TopologicalSpace G] [ChartedSpace E G] [Group G] [LieGroup (𝓘(ℝ, E)) ⊤ G]
    (e : L ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, E)) G)
    (Exp : GroupLieAlgebra (𝓘(ℝ, E)) G → G)
    (chart : GroupLieAlgebra (𝓘(ℝ, E)) G ≃ₜ G) (hchart : ∀ x, chart x = Exp x)
    {J : Type*} [Fintype J] (b : Basis J ℝ L) {K : Set G} (hK : IsCompact K) :
    ∃ R : ℝ, 0 ≤ R ∧ K ⊆ exponentialCoordinateBox (Exp ∘ e) b R := by
…

Mentions: OAI.PolycyclicRecognition.exponentialCoordinateBox

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_compact_semidirect_word_bound line 66

Source documentation

Compact semidirect increments have the same polynomial endpoint bound. The only path restriction is containment of their actual Cartan prefix heights.

theorem exists_compact_semidirect_word_bound
    (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
    (γ : M.Bases) {K : Set (N × D)} (hK : IsCompact K)
    (hφ : ∀ d, φ d = M.adjointGroupAutomorphism T eN ExpN hExpN
      (by rw [← show chartN = ExpN from funext hchartN]; exact chartN.bijective) dynkinN
      (cartanLog H eD ExpD
        (by rw [← show chartD = ExpD from funext hchartD]; exact chartD.bijective) d)) :
    ∃ (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 →
      ∀ r : ℝ, 0 ≤ r → ∀ (m : ℕ) (u : ℕ → N) (v : ℕ → D),
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.cartanLog, OAI.PolycyclicRecognition.IsMaximizingColumnBasis, OAI.PolycyclicRecognition.wordListCoordinates