WordLevelClassification.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Different multiplicities and the orthogonal word-level decomposition

Source and target word levels have independent Hilbert multiplicity spaces. Their scalar slices are bounded endpoint intertwiners, so unequal degrees vanish by the completed endpoint classification.

def OAI.KadisonSimilarity.crossMultiplicitySlice line 26
Source documentation
A bounded scalar multiplicity slice with independently typed source and target multiplicities.
```
def crossMultiplicitySlice
    (Y : HilbertTensor Gsource H →L[ℂ] HilbertTensor Gtarget K)
    (a : Gsource) (b : Gtarget) : H →L[ℂ] K :=
…
```
Mentions: OAI.KadisonSimilarity.HilbertTensor

theorem OAI.KadisonSimilarity.crossMultiplicitySlice_intertwines line 33

Source documentation

Distinct source and target multiplicities do not affect the tensor intertwining calculation.

theorem crossMultiplicitySlice_intertwines
    (Y : HilbertTensor Gsource H →L[ℂ] HilbertTensor Gtarget K)
    (S : H →L[ℂ] H) (T : K →L[ℂ] K)
    (hY : Y.comp (hilbertTensorLift S) = (hilbertTensorLift T).comp Y)
    (a : Gsource) (b : Gtarget) :
    (crossMultiplicitySlice Y a b).comp S = T.comp (crossMultiplicitySlice Y a b) := by
…

Mentions: OAI.KadisonSimilarity.HilbertTensor, OAI.KadisonSimilarity.hilbertTensorLift, OAI.KadisonSimilarity.crossMultiplicitySlice

theorem OAI.KadisonSimilarity.inner_crossMultiplicitySlice line 50

Source documentation

Cross-multiplicity slices are the actual elementary tensor coefficients.

theorem inner_crossMultiplicitySlice
    (Y : HilbertTensor Gsource H →L[ℂ] HilbertTensor Gtarget K)
    (a : Gsource) (b : Gtarget) (x : H) (z : K) :
    inner ℂ z (crossMultiplicitySlice Y a b x) =
      inner ℂ (hilbertTensorInsert b z) (Y (hilbertTensorInsert a x)) := by
…

Mentions: OAI.KadisonSimilarity.HilbertTensor, OAI.KadisonSimilarity.crossMultiplicitySlice, OAI.KadisonSimilarity.hilbertTensorInsert

theorem OAI.KadisonSimilarity.crossMultiplicitySlice_ext line 81
Source documentation
All cross-multiplicity slices determine the entire bounded operator.
```
theorem crossMultiplicitySlice_ext
    (Y Z : HilbertTensor Gsource H →L[ℂ] HilbertTensor Gtarget K)
    (hslice : ∀ a b, crossMultiplicitySlice Y a b = crossMultiplicitySlice Z a b) : Y = Z := by
…
```
Mentions: OAI.KadisonSimilarity.HilbertTensor, OAI.KadisonSimilarity.crossMultiplicitySlice
theorem OAI.KadisonSimilarity.crossMultiplicitySlice_zero line 90
structure OAI.KadisonSimilarity.CrossMultiplicityMatrixCovariance line 105
Source documentation
Actual word covariance for an operator between independent multiplicity spaces. The word formulas refer only to the common endpoint and tail factors.
```
structure CrossMultiplicityMatrixCovariance
    (R : MatrixHilbertStage (E := E) (F := F) (α := α)) (J : F →ₗᵢ⋆[ℂ] F)
…
```
Mentions: OAI.KadisonSimilarity.MatrixHilbertStage
def OAI.KadisonSimilarity.CrossMultiplicityMatrixCovariance.slice line 128
Source documentation
Actual covariance passes to a scalar cross-multiplicity slice.
```
def CrossMultiplicityMatrixCovariance.slice
    {R : MatrixHilbertStage (E := E) (F := F) (α := α)} {J : F →ₗᵢ⋆[ℂ] F}
…
```
Mentions: OAI.KadisonSimilarity.MatrixHilbertStage
theorem OAI.KadisonSimilarity.crossMultiplicity_intertwiner_zero_of_schurWeyl line 145
Source documentation
The unequal-degree theorem applies with entirely different source and target multiplicity Hilbert spaces.
```
theorem crossMultiplicity_intertwiner_zero_of_schurWeyl
    (T : TracialMatrixTower (E := E) (F := F) (A := A))
…
```
Mentions: OAI.KadisonSimilarity.TracialMatrixTower