WordBasisCoordinates.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Maximizing actual word bases

Invertible selections from the coordinate matrix are exactly the actual word bases. Thus the finite maximizing-basis argument applies to the Lie word list.

def OAI.PolycyclicRecognition.wordListCoordinates line 24
theorem OAI.PolycyclicRecognition.wordBasis_det_ne_zero line 27
theorem OAI.PolycyclicRecognition.columnCoordinates_eq_wordBasis_repr line 41
Source documentation
The matrix coordinates agree with the intrinsic coordinates in the selected word basis.
```
theorem columnCoordinates_eq_wordBasis_repr (β : WordBasisSelections X S) (y : S) :
    columnCoordinates (wordListCoordinates X S b₀) β.val y =
      (WordBasisSelections.basis X S β).equivFun (evalBracketWord X y) := by
…
```
Mentions: OAI.PolycyclicRecognition.WordBasisSelections, OAI.PolycyclicRecognition.columnCoordinates, OAI.PolycyclicRecognition.wordListCoordinates, OAI.PolycyclicRecognition.WordBasisSelections.basis, OAI.PolycyclicRecognition.evalBracketWord
def OAI.PolycyclicRecognition.wordBasisOfDet line 56
Source documentation
An invertible coordinate selection gives precisely the actual word basis needed for the finite family, including dimension zero.
```
def wordBasisOfDet (w : Fin (finrank ℝ L) → S)
    (hw : (columnBasisMatrix (wordListCoordinates X S b₀) w).det ≠ 0) :
    WordBasisSelections X S := by
…
```
Mentions: OAI.PolycyclicRecognition.columnBasisMatrix, OAI.PolycyclicRecognition.wordListCoordinates, OAI.PolycyclicRecognition.WordBasisSelections
theorem OAI.PolycyclicRecognition.wordBasisOfDet_val line 67
theorem OAI.PolycyclicRecognition.exists_maximizing_wordBasis line 73
Source documentation
Maximizing over actual bases also maximizes over every invertible column selection. This connects the intrinsic list to the box coordinate estimates.
```
theorem exists_maximizing_wordBasis [Nonempty (WordBasisSelections X S)]
    (cost : S → ℝ) : ∃ β : WordBasisSelections X S,
      IsMaximizingColumnBasis (wordListCoordinates X S b₀) cost β.val := by
…
```
Mentions: OAI.PolycyclicRecognition.WordBasisSelections, OAI.PolycyclicRecognition.IsMaximizingColumnBasis, OAI.PolycyclicRecognition.wordListCoordinates