MatrixTest.lean`

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Polynomial evaluation and actual matrix test operators.

theorem OAI.Kaplansky.actualAlgebraWord_eval line 17
Source documentation
Algebraic words in the constructed bounded-product generators evaluate as the actual Hilbert-shift words, on arbitrary Hilbert vectors.
```
theorem actualAlgebraWord_eval (z : ActualTestIndex) (w : List (Bool × Fin 24)) (v : ActualHilbert z) :
    algebraStarWord actualBoundedGenerator w z v =
      applyWord (shiftLetter (fun i j => actualTestOperator i z j)
        (fun i j => actualTestOperator_norm i z j)) w v := by
…
```
Mentions: OAI.Kaplansky.ActualTestIndex, OAI.Kaplansky.ActualHilbert, OAI.Kaplansky.algebraStarWord, OAI.Kaplansky.actualBoundedGenerator, OAI.Kaplansky.applyWord, OAI.Kaplansky.shiftLetter, OAI.Kaplansky.actualTestOperator, OAI.Kaplansky.actualTestOperator_norm
theorem OAI.Kaplansky.actualAlgebraPolynomial_eval line 39
Source documentation
Exact representation of the finitely supported polynomial supplied by density, before restriction to the bottom-level bundle.
```
theorem actualAlgebraPolynomial_eval (z : ActualTestIndex) (p : StarWordPolynomial 24)
    (v : ActualHilbert z) :
    actualRepresentation z (generatedWordPolynomial actualBoundedGenerator p) v =
      ∑ w ∈ p.support, p w • applyWord (shiftLetter (fun i j => actualTestOperator i z j)
        (fun i j => actualTestOperator_norm i z j)) w v := by
…
```
Mentions: OAI.Kaplansky.ActualTestIndex, OAI.Kaplansky.StarWordPolynomial, OAI.Kaplansky.ActualHilbert, OAI.Kaplansky.actualRepresentation, OAI.Kaplansky.generatedWordPolynomial, OAI.Kaplansky.actualBoundedGenerator, OAI.Kaplansky.applyWord, OAI.Kaplansky.shiftLetter, OAI.Kaplansky.actualTestOperator, OAI.Kaplansky.actualTestOperator_norm
theorem OAI.Kaplansky.actualRepresentation_matrix_column line 53
theorem OAI.Kaplansky.actualRepresentation_matrix_entry_close line 69
theorem OAI.Kaplansky.actualPolynomialMatrix_action line 80
Source documentation
The matrix entries supplied by density and their extracted term list have precisely the same action on the matching actual test Hilbert space.
```
theorem actualPolynomialMatrix_action {m n : ℕ} (hm : 0<m)
    (p : Fin m → Fin n → StarWordPolynomial 24)
    (y : SmoothTestBase m (matrixPolynomialDegree p))
    (v : MatrixTowerHilbert (testSequenceStage m (matrixPolynomialDegree p)) n y) :
    operatorMatrixAction (fun row col => actualRepresentation
      ⟨⟨m,hm⟩,⟨matrixPolynomialDegree p,matrixPolynomialDegree_pos p⟩,y⟩
      (generatedWordPolynomial actualBoundedGenerator (p row col))) v =
    matrixPolynomialAction (testSequenceStep (R := matrixPolynomialDegree p) hm)
…
```
Mentions: OAI.Kaplansky.StarWordPolynomial, OAI.Kaplansky.SmoothTestBase, OAI.Kaplansky.matrixPolynomialDegree, OAI.Kaplansky.MatrixTowerHilbert, OAI.Kaplansky.testSequenceStage, OAI.Kaplansky.operatorMatrixAction, OAI.Kaplansky.actualRepresentation, OAI.Kaplansky.matrixPolynomialDegree_pos, OAI.Kaplansky.generatedWordPolynomial, OAI.Kaplansky.actualBoundedGenerator, OAI.Kaplansky.matrixPolynomialAction, OAI.Kaplansky.testSequenceStep