CartanWordPacking.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Ambient packing for controlled Cartan word endpoints

A positive cell in the product of the actual factors is translated by fixed word lifts. These cells are disjoint after testing their projections in the ambient metric. The word-thickening theorem encloses them in one product of boxes, with the exact support exponential and polynomial radii.

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_ambient_word_packing_bound line 50

Source documentation

An ambient separated set of controlled word endpoints satisfies the support-exponential volume bound. The source cell has positive finite mass; all remaining dependence on word length is polynomial.

theorem exists_ambient_word_packing_bound
    (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
    (γ : M.Bases) {K : Set G} (hK : IsCompact K) {ρ : ℝ} (hρ : 0 < ρ)
    (hφ : ∀ d, F.action d = M.adjointGroupAutomorphism T F.N.equiv F.ExpN F.isExpN
      (by rw [← show chartN = F.ExpN from funext hchartN]; exact chartN.bijective) dynkinN
      (cartanLog H F.D.equiv F.ExpD
        (by rw [← show chartD = F.ExpD from funext hchartD]; exact chartD.bijective) d)) :
    ∃ (Q : ℝ≥0∞) (B C A : ℝ) (q c : ℕ), 0 < Q ∧ Q < ⊤ ∧
      0 < B ∧ 0 ≤ C ∧ 0 ≤ A ∧ ∀ {E : Set W}, IsCompact E → E.Nonempty →
      ∀ r : ℝ, 0 ≤ r → ∀ (m : ℕ) (s : Finset G),
      (∀ x ∈ s, ∀ y ∈ s, x ≠ y → ρ ≤ dist x y) →
      (∀ x ∈ s, ∃ u : ℕ → G, (∀ i < m, u i ∈ K) ∧
…

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

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_ambient_word_polynomial_packing line 131

Source documentation

The ambient word endpoint count has a uniform polynomial prefactor and the exact Cartan support exponential.

theorem exists_ambient_word_polynomial_packing
    (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
    (γ : M.Bases) {K : Set G} (hK : IsCompact K) {ρ : ℝ} (hρ : 0 < ρ)
    (hφ : ∀ d, F.action d = M.adjointGroupAutomorphism T F.N.equiv F.ExpN F.isExpN
      (by rw [← show chartN = F.ExpN from funext hchartN]; exact chartN.bijective) dynkinN
      (cartanLog H F.D.equiv F.ExpD
        (by rw [← show chartD = F.ExpD from funext hchartD]; exact chartD.bijective) d)) :
    ∃ (D : ℝ) (k : ℕ), 0 < D ∧ ∀ {E : Set W}, IsCompact E → E.Nonempty →
      ∀ r : ℝ, 0 ≤ r → ∀ (m : ℕ) (s : Finset G),
      (∀ x ∈ s, ∀ y ∈ s, x ≠ y → ρ ≤ dist x y) →
      (∀ x ∈ s, ∃ u : ℕ → G, (∀ i < m, u i ∈ K) ∧
        (∀ i ≤ m, ∃ w ∈ E, (π (wordPrefix u i)).toAdd = r • w) ∧ wordPrefix u m = x) →
…

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