CartanFixedSlicePacking.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Lower packing for actual Cartan slices

The nilpotent parameter measure has its computed word-box volume. Its invariance under the full Cartan action makes one finite packing constant work at every Cartan position and every translated basepoint.

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_uniform_fixedSlice_packing line 40

Source documentation

The fixed-slice packing constant is finite and independent of basepoint, Cartan position and compact endpoint set. The same Haar measure has the exact weighted-box formula from the Lie model.

theorem exists_uniform_fixedSlice_packing
    (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
    (hφ : ∀ d, φ d = M.adjointGroupAutomorphism T eN Exp hExp hbij dynkin (logD d))
    (hconj : ∀ d u, ι (φ d u) = κ d * ι u * (κ d)⁻¹)
    (hι : Topology.IsClosedEmbedding ι) {r : ℝ} (hr : 0 < r) :
    ∃ (μ : Measure N) (C : ℝ≥0∞), μ.IsHaarMeasure ∧ C < ⊤ ∧
      (∀ (cost : M.wordList → ℝ) (β : M.Bases) (s R : ℝ), 0 ≤ R →
        μ (exponentialCoordinateBox (Exp ∘ eN)
          (exponentialRescaleBasis (WordBasisSelections.basis M.letter M.wordList β)
            (fun i => cost (β.val i)) s) R) =
          ENNReal.ofReal |(columnBasisMatrix (wordListCoordinates M.letter M.wordList b₀) β.val).det| *
            ENNReal.ofReal (Real.exp (s * columnBasisWeight cost β.val)) *
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.exponentialCoordinateBox, OAI.PolycyclicRecognition.exponentialRescaleBasis, OAI.PolycyclicRecognition.WordBasisSelections.basis, OAI.PolycyclicRecognition.columnBasisMatrix, OAI.PolycyclicRecognition.wordListCoordinates, OAI.PolycyclicRecognition.columnBasisWeight