OrthogonalWordLevels.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Orthogonal word-level inclusions turn the proved off-diagonal block vanishing into actual preservation of each full word level.

structure OAI.KadisonSimilarity.OrthogonalWordLevels line 17
Source documentation
Actual isometric word inclusions with orthogonal ranges and dense linear span. No operator invariance is built into these geometric data.
```
structure OrthogonalWordLevels (W : ℕ → Type*) [∀ n, NormedAddCommGroup (W n)]
    [∀ n, InnerProductSpace ℂ (W n)] (H : Type*) [NormedAddCommGroup H]
    [InnerProductSpace ℂ H] where
…
```
def OAI.KadisonSimilarity.OrthogonalWordLevels.coordinate line 28
def OAI.KadisonSimilarity.OrthogonalWordLevels.block line 30
theorem OAI.KadisonSimilarity.OrthogonalWordLevels.norm_block_le line 34
Source documentation
Orthogonal word-block compression does not increase operator norm.
```
theorem norm_block_le (Y : H →L[ℂ] H) (m n : ℕ) : ‖U.block Y m n‖ ≤ ‖Y‖ := by
…
```
theorem OAI.KadisonSimilarity.OrthogonalWordLevels.coordinate_inclusion_self line 53
theorem OAI.KadisonSimilarity.OrthogonalWordLevels.coordinate_inclusion_ne line 57
theorem OAI.KadisonSimilarity.OrthogonalWordLevels.map_eq_zero_of_levels line 68
Source documentation
A continuous linear map is determined by its values on the actual word inclusions because their linear span is dense.
```
theorem map_eq_zero_of_levels {K : Type*} [NormedAddCommGroup K] [NormedSpace ℂ K]
    (f : H →L[ℂ] K) (hf : ∀ n x, f (U.inclusion n x) = 0) : f = 0 := by
…
```
theorem OAI.KadisonSimilarity.OrthogonalWordLevels.eq_zero_of_coordinates line 82
Source documentation
All word-level coordinates separate vectors in the ambient Hilbert space.
```
theorem eq_zero_of_coordinates (z : H) (hz : ∀ n, U.coordinate n z = 0) : z = 0 := by
…
```

theorem OAI.KadisonSimilarity.OrthogonalWordLevels.block_intertwines line 95

Source documentation

Compressing a global commutation identity yields the actual block intertwining. Adjoint covariance of the target inclusion supplies its coordinate covariance.

theorem block_intertwines (Y A : H →L[ℂ] H) {n m : ℕ}
    (S : W n →L[ℂ] W n) (T : W m →L[ℂ] W m)
    (hY : Y.comp A = A.comp Y)
    (hsource : A.comp (U.inclusion n).toContinuousLinearMap =
      (U.inclusion n).toContinuousLinearMap.comp S)
    (htarget : A.adjoint.comp (U.inclusion m).toContinuousLinearMap =
      (U.inclusion m).toContinuousLinearMap.comp T.adjoint) :
    (U.block Y m n).comp S = T.comp (U.block Y m n) := by
…

theorem OAI.KadisonSimilarity.OrthogonalWordLevels.preserves_of_offDiagonal_zero line 117
Source documentation
Vanishing of the off-diagonal blocks implies actual preservation of every word level; this uses dense span, rather than an assumed direct-sum model.
```
theorem preserves_of_offDiagonal_zero (Y : H →L[ℂ] H)
    (hzero : ∀ m n, m ≠ n → U.block Y m n = 0) (n : ℕ) :
    Y.comp (U.inclusion n).toContinuousLinearMap =
      (U.inclusion n).toContinuousLinearMap.comp (U.block Y n n) := by
…
```

abbrev OAI.KadisonSimilarity.MultiplicityWordSpace line 150

Source documentation

The actual space of one word level, including its degree-dependent multiplicity.

abbrev MultiplicityWordSpace (G : ℕ → Type*) [∀ n, NormedAddCommGroup (G n)]
    [∀ n, InnerProductSpace ℂ (G n)] (E F : Type u)
    [NormedAddCommGroup E] [InnerProductSpace ℂ E]
    [NormedAddCommGroup F] [InnerProductSpace ℂ F] (n : ℕ) :=
…

structure OAI.KadisonSimilarity.WordLevelMatrixActions line 159
Source documentation
Raw action data on the ambient word Hilbert space. Both ordinary and adjoint inclusion covariance are explicit, as supplied by reducing free-word levels. No operator block vanishing is included.
```
structure WordLevelMatrixActions
    (T : TracialMatrixTower (E := E) (F := F) (A := A))
…
```
Mentions: OAI.KadisonSimilarity.TracialMatrixTower
def OAI.KadisonSimilarity.WordLevelMatrixActions.blockCovariance line 202
Source documentation
Ambient commutation and the actual inclusion identities supply the whole cross-multiplicity covariance of every compressed word block.
```
def WordLevelMatrixActions.blockCovariance (s k l : ℕ) :
    CrossMultiplicityMatrixCovariance (T.stage s) T.conjugation T.traceVector (U.block Y l k) where
…
```
Mentions: OAI.KadisonSimilarity.CrossMultiplicityMatrixCovariance

theorem OAI.KadisonSimilarity.word_levels_preserved_of_schurWeyl line 214

Source documentation

Global word-level preservation follows from Schur--Weyl and ambient commutation. Off-diagonal block vanishing is proved, not supplied.

theorem word_levels_preserved_of_schurWeyl
    (spanning : ∀ k l s,
      SchurWeylMultilinearSpanning (Option (Fin k ⊕ Fin l)) (A s))
    (hcontraction : ∀ k l s (π : Equiv.Perm (Option (Fin k ⊕ Fin l))) v,
      normalizedPermutationContraction π (fun i => T.inclusion s (v i)) =
        normalizedPermutationContraction π v)
    (labels : ∀ k l s, Option (Fin k ⊕ Fin l) → A s)
    (hlabels : ∀ k l s, Function.Injective (labels k l s)) (n : ℕ) :
    Y.comp (U.inclusion n).toContinuousLinearMap =
      (U.inclusion n).toContinuousLinearMap.comp (U.block Y n n) := by
…

Mentions: OAI.KadisonSimilarity.SchurWeylMultilinearSpanning, OAI.KadisonSimilarity.normalizedPermutationContraction