CartanBoxExponents.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Exact box exponents for the Cartan word model

The compact-template support equals the maximum of the determinant exponents of the actual word boxes. This connects the Lie-algebra construction to the Euclidean coordinate-volume formula.

def OAI.PolycyclicRecognition.CartanWordModel.supportIn line 32
Source documentation
Support data in the fixed Euclidean coordinates on height.
```
def supportIn : SupportDatum W (Fin M.letterCount) M.Bases :=
…
```
Mentions: OAI.PolycyclicRecognition.SupportDatum
def OAI.PolycyclicRecognition.CartanWordModel.boxCost line 36
Source documentation
The exponent of a word is the sum of the separately supported letters.
```
def boxCost (E : Set W) (w : M.wordList) : ℝ :=
…
```
theorem OAI.PolycyclicRecognition.CartanWordModel.columnBasisWeight_boxCost line 40
Source documentation
The determinant exponent of each basis is its template support sum.
```
theorem columnBasisWeight_boxCost (E : Set W) (β : M.Bases) :
    columnBasisWeight (M.boxCost T hunimod e E) β.val =
      (M.supportIn T hunimod e).basisTemplateSupport E β := by
…
```
Mentions: OAI.PolycyclicRecognition.columnBasisWeight

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_maximizing_box_basis line 48

Source documentation

Maximizing the finite word-box determinant gives exactly P(E).

theorem exists_maximizing_box_basis
    (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
    (E : Set W) : ∃ β : M.Bases,
      IsMaximizingColumnBasis (wordListCoordinates M.letter M.wordList b₀)
        (M.boxCost T hunimod e E) β.val ∧
      columnBasisWeight (M.boxCost T hunimod e E) β.val =
        (M.supportIn T hunimod e).templateSupport E := by
…

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

theorem OAI.PolycyclicRecognition.CartanWordModel.columnBasisWeight_eq_templateSupport_of_maximizing line 66

Source documentation

Every maximizing basis has the same template exponent, including ties.

theorem columnBasisWeight_eq_templateSupport_of_maximizing
    (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
    (E : Set W) (β : M.Bases)
    (hβ : IsMaximizingColumnBasis (wordListCoordinates M.letter M.wordList b₀)
      (M.boxCost T hunimod e E) β.val) :
    columnBasisWeight (M.boxCost T hunimod e E) β.val =
      (M.supportIn T hunimod e).templateSupport E := by
…

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

theorem OAI.PolycyclicRecognition.CartanWordModel.volume_maximizing_coordinateBox line 82

Source documentation

The volume of a maximizing coordinate box has precisely the template support exponent, with its actual unscaled basis determinant.

theorem volume_maximizing_coordinateBox
    (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
    (E : Set W) (β : M.Bases)
    (hβ : columnBasisWeight (M.boxCost T hunimod e E) β.val =
      (M.supportIn T hunimod e).templateSupport E) (r R : ℝ) :
    volume (weightedCoordinateBox (wordListCoordinates M.letter M.wordList b₀)
      (M.boxCost T hunimod e E) β.val r R) =
      ENNReal.ofReal |(columnBasisMatrix (wordListCoordinates M.letter M.wordList b₀) β.val).det| *
      ENNReal.ofReal (Real.exp (r * (M.supportIn T hunimod e).templateSupport E)) *
      ENNReal.ofReal (2 * R) ^ finrank ℝ (cartanRootIdeal H) := by
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.columnBasisWeight, OAI.PolycyclicRecognition.weightedCoordinateBox, OAI.PolycyclicRecognition.wordListCoordinates, OAI.PolycyclicRecognition.columnBasisMatrix

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_uniform_wordBasis_determinant_bounds line 96
Source documentation
Finiteness of the actual basis family gives positive uniform determinant bounds, independent of every height template and scaling parameter.
```
theorem exists_uniform_wordBasis_determinant_bounds
    (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H)) :
    ∃ c C : ℝ, 0 < c ∧ 0 < C ∧ ∀ β : M.Bases,
      c ≤ |(columnBasisMatrix (wordListCoordinates M.letter M.wordList b₀) β.val).det| ∧
      |(columnBasisMatrix (wordListCoordinates M.letter M.wordList b₀) β.val).det| ≤ C := by
…
```
Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.columnBasisMatrix, OAI.PolycyclicRecognition.wordListCoordinates