CartanWordVolume.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Upper volume of controlled word endpoints

The semidirect-product word estimate and the exact Haar volume of Cartan boxes give a polynomial prefactor times the template support exponential. This is an upper bound for the nilpotent coordinate of actual word endpoints.

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_semidirect_word_volume_bound line 44

Source documentation

Every set of controlled nilpotent endpoint coordinates has the claimed exponential upper rate, with a polynomial prefactor uniform in the template.

theorem exists_semidirect_word_volume_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) :
    ∃ (μ : Measure N) (C : ℝ) (q : ℕ), μ.IsHaarMeasure ∧ 0 ≤ C ∧
      ∀ {E : Set W}, IsCompact E → E.Nonempty → ∀ (γ : M.Bases) (r : ℝ), 0 ≤ r →
      ∀ (m : ℕ) (S : Set N),
      (∀ z ∈ S, ∃ (u : ℕ → N) (v : ℕ → D),
        (∀ i < m, u i ∈ exponentialCoordinateBox (ExpN ∘ eN)
          (WordBasisSelections.basis M.letter M.wordList γ) RN) ∧
        (∀ i < m, v i ∈ exponentialCoordinateBox (ExpD ∘ eD) (finBasis ℝ H) RD) ∧
…

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