Words.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Word propagation through Hilbert shifts and normalized tuple operators.

def OAI.Kaplansky.applyWord line 18
Source documentation
Apply a word of operators, in the multiplication order used by noncommutative polynomials. A generator and its adjoint are separate letters of the alphabet.
```
def applyWord (T : ι → Module.End 𝕜 V) : List ι → V → V
  | [], v => v
  | a::w, v => T a (applyWord T w v)
```
theorem OAI.Kaplansky.word_mem_level line 22
theorem OAI.Kaplansky.polynomial_mem_level line 30
def OAI.Kaplansky.hilbertLevels line 50
Source documentation
The actual first k+1 levels of the Hilbert sum.
```
def hilbertLevels (k : ℕ) : Submodule ℂ (FiberHilbertSum E) where
…
```
Mentions: OAI.Kaplansky.FiberHilbertSum
theorem OAI.Kaplansky.hilbertLevels_mono line 57
def OAI.Kaplansky.shiftLetter line 64
Source documentation
False letters are generators; true letters are their actual adjoints.
```
def shiftLetter (a : Bool × Fin n) : Module.End ℂ (FiberHilbertSum E) :=
…
```
Mentions: OAI.Kaplansky.FiberHilbertSum
theorem OAI.Kaplansky.shiftLetter_mem_level line 68
theorem OAI.Kaplansky.shift_word_from_bottom line 83

theorem OAI.Kaplansky.shift_polynomial_from_bottom line 92

Source documentation

Actual operator *-polynomials of degree R send the bottom fiber into levels zero through R; no global Hilbert-bundle trivialization is assumed.

theorem shift_polynomial_from_bottom {K : Type*} (s : Finset K)
    (words : K → List (Bool × Fin n)) (coeff : K → ℂ) (R : ℕ)
    (hdeg : ∀ j ∈ s, (words j).length ≤ R) (v : E 0) :
    (∑ j ∈ s, coeff j • applyWord (shiftLetter T hT) (words j) (lp.single 2 0 v)) ∈
      hilbertLevels R := by
…

Mentions: OAI.Kaplansky.applyWord, OAI.Kaplansky.shiftLetter, OAI.Kaplansky.hilbertLevels

def OAI.Kaplansky.NormalizedHermitianTuple.operator line 117
Source documentation
Actual bounded operators on the finite-dimensional Hilbert fibers.
```
def operator (T : NormalizedHermitianTuple E F) (i : Fin 24) : E →L[ℂ] F :=
…
```
Mentions: OAI.Kaplansky.NormalizedHermitianTuple
theorem OAI.Kaplansky.NormalizedHermitianTuple.operator_adjoint line 120
theorem OAI.Kaplansky.NormalizedHermitianTuple.operator_column line 127
theorem OAI.Kaplansky.NormalizedHermitianTuple.operator_row line 133
theorem OAI.Kaplansky.NormalizedHermitianTuple.operator_norm_le line 153