BundlePolynomials.lean`

24 declarations, 0 contain sorry, 0 declared as axioms

Bundle matrix polynomial evaluation, Hilbert isometries, and polynomial action.

structure OAI.Kaplansky.BoundedMatrixTerm line 18
Source documentation
One term of a rectangular star polynomial, with its actual word and its degree bound. Zero coefficients and empty words are allowed.
```
structure BoundedMatrixTerm (m n R : ℕ) where
…
```
def OAI.Kaplansky.towerRetainedStage line 28
Source documentation
The finite direct sum of the retained stages, for each matrix row.
```
def towerRetainedStage (a : ℕ → LineStage K) (m R : ℕ) : LineStage K :=
…
```
Mentions: OAI.Kaplansky.LineStage
def OAI.Kaplansky.towerInputStage line 32
Source documentation
The bottom bundle repeated once per matrix column.
```
def towerInputStage (a : ℕ → LineStage K) (n : ℕ) : LineStage K :=
…
```
Mentions: OAI.Kaplansky.LineStage
def OAI.Kaplansky.bundleMatrixTerm line 37
def OAI.Kaplansky.bundleMatrixPolynomial line 49
Source documentation
The intrinsic finite matrix restriction. Its continuity is proved from actual normalized bundle maps and adjoints, including the constant term.
```
def bundleMatrixPolynomial {m n R : ℕ} {T : Type*} (s : Finset T)
    (t : T → BoundedMatrixTerm m n R) :
    ContinuousStageMap (towerInputStage a n) (towerRetainedStage a m R) :=
…
```
Mentions: OAI.Kaplansky.BoundedMatrixTerm, OAI.Kaplansky.ContinuousStageMap, OAI.Kaplansky.towerInputStage, OAI.Kaplansky.towerRetainedStage
theorem OAI.Kaplansky.bundleMatrixPolynomial_continuous line 54
abbrev OAI.Kaplansky.MatrixPolynomialTermIndex line 61
def OAI.Kaplansky.matrixPolynomialDegree line 64
theorem OAI.Kaplansky.matrixPolynomialDegree_pos line 67
def OAI.Kaplansky.matrixPolynomialTerm line 72
Source documentation
The common positive degree bound and the actual terms of a finite rectangular polynomial matrix are produced from its entries.
```
def matrixPolynomialTerm {m n : ℕ} (p : Fin m → Fin n → StarWordPolynomial 24)
    (k : MatrixPolynomialTermIndex p) : BoundedMatrixTerm m n (matrixPolynomialDegree p) where
…
```
Mentions: OAI.Kaplansky.StarWordPolynomial, OAI.Kaplansky.MatrixPolynomialTermIndex, OAI.Kaplansky.BoundedMatrixTerm, OAI.Kaplansky.matrixPolynomialDegree
theorem OAI.Kaplansky.matrixPolynomialTerm_sum line 81
def OAI.Kaplansky.retainedRowHilbert line 103

theorem OAI.Kaplansky.bundleMatrixTerm_shift_eval line 111

Source documentation

A matrix monomial has exactly its claimed shift-operator action in each output row. No unspecified representation or evaluation is used.

theorem bundleMatrixTerm_shift_eval {m n R : ℕ} (t : BoundedMatrixTerm m n R)
    (y : ProjectiveProduct K) (v : (towerInputStage a n).Fiber y) (row : Fin m) :
    retainedRowHilbert a m R y row ((bundleMatrixTerm X t).map y v) =
      if t.row=row then t.coeff •
        applyWord (shiftLetter (fun i j => towerOperator X i y j)
          (fun i j => towerOperator_norm X i y j)) t.word
            (lp.single 2 0 (LineStage.sumProj (fun _ : Fin n => a 0) t.col y v)) else 0 := by
…

Mentions: OAI.Kaplansky.BoundedMatrixTerm, OAI.Kaplansky.towerInputStage, OAI.Kaplansky.retainedRowHilbert, OAI.Kaplansky.bundleMatrixTerm, OAI.Kaplansky.applyWord, OAI.Kaplansky.shiftLetter, OAI.Kaplansky.towerOperator, OAI.Kaplansky.towerOperator_norm, OAI.Kaplansky.LineStage.sumProj

theorem OAI.Kaplansky.bundleMatrixPolynomial_shift_eval line 137

Source documentation

Exact evaluation agreement for the entire rectangular polynomial, including all coefficients, rows, columns, constants, and adjoints.

theorem bundleMatrixPolynomial_shift_eval {m n R : ℕ} {T : Type*}
    (s : Finset T) (t : T → BoundedMatrixTerm m n R) (y : ProjectiveProduct K)
    (v : (towerInputStage a n).Fiber y) (row : Fin m) :
    retainedRowHilbert a m R y row ((bundleMatrixPolynomial X s t).map y v) =
      ∑ k ∈ s, if (t k).row=row then (t k).coeff •
        applyWord (shiftLetter (fun i j => towerOperator X i y j)
          (fun i j => towerOperator_norm X i y j)) (t k).word
            (lp.single 2 0 (LineStage.sumProj (fun _ : Fin n => a 0) (t k).col y v)) else 0 := by
…

Mentions: OAI.Kaplansky.BoundedMatrixTerm, OAI.Kaplansky.towerInputStage, OAI.Kaplansky.retainedRowHilbert, OAI.Kaplansky.bundleMatrixPolynomial, OAI.Kaplansky.applyWord, OAI.Kaplansky.shiftLetter, OAI.Kaplansky.towerOperator, OAI.Kaplansky.towerOperator_norm, OAI.Kaplansky.LineStage.sumProj

abbrev OAI.Kaplansky.MatrixTowerHilbert line 150
def OAI.Kaplansky.retainedMatrixHilbertMap line 153
theorem OAI.Kaplansky.retainedMatrixHilbert_inner line 165
def OAI.Kaplansky.retainedMatrixHilbertIsometry line 175
def OAI.Kaplansky.inputMatrixHilbertMap line 180
theorem OAI.Kaplansky.inputMatrixHilbert_inner line 197
def OAI.Kaplansky.inputMatrixHilbertIsometry line 206
def OAI.Kaplansky.matrixPolynomialAction line 213
Source documentation
Direct evaluated matrix action on Hilbert vectors, with every term placed in its specified row and applied to its specified input column.
```
def matrixPolynomialAction {m n R : ℕ} {T : Type*} (s : Finset T)
    (t : T → BoundedMatrixTerm m n R) (y : ProjectiveProduct K)
    (v : MatrixTowerHilbert a n y) : MatrixTowerHilbert a m y :=
…
```
Mentions: OAI.Kaplansky.BoundedMatrixTerm, OAI.Kaplansky.MatrixTowerHilbert
theorem OAI.Kaplansky.bundleMatrixPolynomial_evaluation line 222
Source documentation
The entire intrinsic matrix restriction agrees exactly with evaluation on bottom-level inputs, through norm-preserving Hilbert embeddings.
```
theorem bundleMatrixPolynomial_evaluation {m n R : ℕ} {T : Type*}
    (s : Finset T) (t : T → BoundedMatrixTerm m n R) (y : ProjectiveProduct K)
    (v : (towerInputStage a n).Fiber y) :
    retainedMatrixHilbertIsometry a m R y ((bundleMatrixPolynomial X s t).map y v) =
      matrixPolynomialAction X s t y (inputMatrixHilbertIsometry a n y v) := by
…
```
Mentions: OAI.Kaplansky.BoundedMatrixTerm, OAI.Kaplansky.towerInputStage, OAI.Kaplansky.retainedMatrixHilbertIsometry, OAI.Kaplansky.bundleMatrixPolynomial, OAI.Kaplansky.matrixPolynomialAction, OAI.Kaplansky.inputMatrixHilbertIsometry
theorem OAI.Kaplansky.bundleMatrixPolynomial_lower_bound line 233
Source documentation
A lower bound for the evaluated operator passes to the actual finite bundle map. The two Hilbert inclusions are proved isometries.
```
theorem bundleMatrixPolynomial_lower_bound {m n R : ℕ} {T : Type*}
    (s : Finset T) (t : T → BoundedMatrixTerm m n R) (y : ProjectiveProduct K) (c : ℝ)
    (h : ∀ v : MatrixTowerHilbert a n y, c*‖v‖ ≤ ‖matrixPolynomialAction X s t y v‖)
    (v : (towerInputStage a n).Fiber y) :
    c*‖v‖ ≤ ‖(bundleMatrixPolynomial X s t).map y v‖ := by
…
```
Mentions: OAI.Kaplansky.BoundedMatrixTerm, OAI.Kaplansky.MatrixTowerHilbert, OAI.Kaplansky.matrixPolynomialAction, OAI.Kaplansky.towerInputStage, OAI.Kaplansky.bundleMatrixPolynomial