WordMultiplicities.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

The actual multiplicity spaces of the alternating tracial words, their normalized repeated-letter inclusions, and the degree-zero identification.

abbrev OAI.KadisonSimilarity.WordMultiplicity line 16
Source documentation
The multiplicity of words with k centered base-algebra letters.
```
abbrev WordMultiplicity (ΩA : B) (k : ℕ) :=
…
```
def OAI.KadisonSimilarity.multiplicityWordInclusion line 21
Source documentation
A unit vector in the centered tensor power inserts the base Hilbert space isometrically into the corresponding multiplicity space.
```
def multiplicityWordInclusion (ΩA : B) {k : ℕ}
    (w : CompletedTensorWord (centeredSubspace ΩA) k) (hw : ‖w‖ = 1) :
    B →ₗᵢ[ℂ] WordMultiplicity ΩA k where
…
```
Mentions: OAI.KadisonSimilarity.CompletedTensorWord, OAI.KadisonSimilarity.centeredSubspace, OAI.KadisonSimilarity.WordMultiplicity
theorem OAI.KadisonSimilarity.multiplicityWordInclusion_apply line 29
def OAI.KadisonSimilarity.repeatedMultiplicityWord line 34
Source documentation
The repeated centered word s ⊗ ⋯ ⊗ s.
```
def repeatedMultiplicityWord (ΩA : B) (s : centeredSubspace ΩA) (k : ℕ) :
    CompletedTensorWord (centeredSubspace ΩA) k :=
…
```
Mentions: OAI.KadisonSimilarity.centeredSubspace, OAI.KadisonSimilarity.CompletedTensorWord
theorem OAI.KadisonSimilarity.norm_repeatedMultiplicityWord line 38
def OAI.KadisonSimilarity.repeatedMultiplicityInclusion line 43
Source documentation
Insertion of a normalized repeated centered letter, with its exact norm.
```
def repeatedMultiplicityInclusion (ΩA : B) (s : centeredSubspace ΩA)
    (hs : ‖s‖ = 1) (k : ℕ) : B →ₗᵢ[ℂ] WordMultiplicity ΩA k :=
…
```
Mentions: OAI.KadisonSimilarity.centeredSubspace, OAI.KadisonSimilarity.WordMultiplicity
theorem OAI.KadisonSimilarity.repeatedMultiplicityInclusion_apply line 48
def OAI.KadisonSimilarity.zeroMultiplicityWord line 54
Source documentation
The empty centered word is the scalar unit in tensor degree zero.
```
def zeroMultiplicityWord (ΩA : B) : CompletedTensorWord (centeredSubspace ΩA) 0 :=
…
```
Mentions: OAI.KadisonSimilarity.CompletedTensorWord, OAI.KadisonSimilarity.centeredSubspace
theorem OAI.KadisonSimilarity.norm_zeroMultiplicityWord line 57
def OAI.KadisonSimilarity.zeroMultiplicityInclusion line 61
Source documentation
The canonical degree-zero inclusion of the base Hilbert space.
```
def zeroMultiplicityInclusion (ΩA : B) : B →ₗᵢ[ℂ] WordMultiplicity ΩA 0 :=
…
```
Mentions: OAI.KadisonSimilarity.WordMultiplicity
theorem OAI.KadisonSimilarity.zeroMultiplicityInclusion_apply line 64
theorem OAI.KadisonSimilarity.zeroMultiplicity_slice_inverse line 71
Source documentation
In degree zero the slice recovers every tensor, as proved from totality of the completed empty word and of elementary Hilbert tensors.
```
theorem zeroMultiplicity_slice_inverse (ΩA : B) :
    (zeroMultiplicityInclusion ΩA).toContinuousLinearMap.comp
      (tensorSlice (zeroMultiplicityWord ΩA)) =
        ContinuousLinearMap.id ℂ (WordMultiplicity ΩA 0) := by
…
```
Mentions: OAI.KadisonSimilarity.zeroMultiplicityInclusion, OAI.KadisonSimilarity.tensorSlice, OAI.KadisonSimilarity.zeroMultiplicityWord, OAI.KadisonSimilarity.WordMultiplicity
theorem OAI.KadisonSimilarity.zeroMultiplicityInclusion_surjective line 99
Source documentation
No extra scalar tensor factor remains at word degree zero.
```
theorem zeroMultiplicityInclusion_surjective (ΩA : B) :
    Function.Surjective (zeroMultiplicityInclusion ΩA) := by
…
```
Mentions: OAI.KadisonSimilarity.zeroMultiplicityInclusion
def OAI.KadisonSimilarity.zeroMultiplicityEquiv line 107
Source documentation
The actual unitary identification of the base space with multiplicity zero.
```
def zeroMultiplicityEquiv (ΩA : B) : B ≃ₗᵢ[ℂ] WordMultiplicity ΩA 0 :=
…
```
Mentions: OAI.KadisonSimilarity.WordMultiplicity
theorem OAI.KadisonSimilarity.zeroMultiplicityEquiv_apply line 111
theorem OAI.KadisonSimilarity.repeatedMultiplicityInclusion_zero line 115
Source documentation
Repeated insertion at degree zero is precisely the canonical unitary.
```
theorem repeatedMultiplicityInclusion_zero (ΩA : B) (s : centeredSubspace ΩA)
    (hs : ‖s‖ = 1) :
    repeatedMultiplicityInclusion ΩA s hs 0 = (zeroMultiplicityEquiv ΩA).toLinearIsometry := by
…
```
Mentions: OAI.KadisonSimilarity.centeredSubspace, OAI.KadisonSimilarity.repeatedMultiplicityInclusion, OAI.KadisonSimilarity.zeroMultiplicityEquiv
def OAI.KadisonSimilarity.zeroMultiplicityOperator line 124
Source documentation
Transport the canonical degree-zero block to an operator on the base space.
```
def zeroMultiplicityOperator (ΩA : B) (T : WordMultiplicity ΩA 0 →L[ℂ] WordMultiplicity ΩA 0) :
    B →L[ℂ] B :=
…
```
Mentions: OAI.KadisonSimilarity.WordMultiplicity
theorem OAI.KadisonSimilarity.zeroMultiplicityOperator_intertwines line 129