WordLevelRepeatedOperators.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Canonical multiplicity operators on repeated-letter words

Compression to one normalized repeated word defines the degree-wise operator. The invariant-intertwiner classification proves that this same operator acts on every repeated-letter word. Adjoint compatibility follows from the concrete compression formula.

def OAI.KadisonSimilarity.wordLevelRepeatedOperator line 31
Source documentation
The canonical degree-wise operator is a concrete compression to one unit repeated word. Its independence of that word is proved below.
```
def wordLevelRepeatedOperator (Y : H →L[ℂ] H) (n : ℕ) : G n →L[ℂ] G n :=
…
```
theorem OAI.KadisonSimilarity.norm_wordLevelRepeatedOperator_le line 36
theorem OAI.KadisonSimilarity.wordLevelRepeatedOperator_adjoint line 45
Source documentation
The canonical compression commutes with taking the adjoint, for every bounded ambient operator, before any invariant-theory hypotheses are imposed.
```
theorem wordLevelRepeatedOperator_adjoint (Y : H →L[ℂ] H) (n : ℕ) :
    wordLevelRepeatedOperator T U Y.adjoint n = (wordLevelRepeatedOperator T U Y n).adjoint := by
…
```
Mentions: OAI.KadisonSimilarity.wordLevelRepeatedOperator
def OAI.KadisonSimilarity.WordLevelMatrixActions.diagonalCovariance line 58
Source documentation
On a diagonal block the cross-multiplicity word covariance is exactly the existing same-multiplicity covariance.
```
def WordLevelMatrixActions.diagonalCovariance (s n : ℕ) :
    MultiplicityMatrixCovariance (T.stage s) T.conjugation T.traceVector (U.block Y n n) where
…
```
Mentions: OAI.KadisonSimilarity.MultiplicityMatrixCovariance

theorem OAI.KadisonSimilarity.wordLevelRepeatedOperator_block_apply line 70

Source documentation

The degree-wise compression acts on every repeated-letter vector in its full diagonal block.

theorem wordLevelRepeatedOperator_block_apply (n : ℕ)
    (spanning : ∀ s, SchurWeylMultilinearSpanning (Option (Fin n ⊕ Fin n)) (A s))
    (hcontraction : ∀ s (π : Equiv.Perm (Option (Fin n ⊕ Fin n))) v,
      normalizedPermutationContraction π (fun i => T.inclusion s (v i)) =
        normalizedPermutationContraction π v)
    (labels : ∀ s, Option (Fin n ⊕ Fin n) → A s)
    (hlabels : ∀ s, Function.Injective (labels s)) (a : G n) (d : E) (r : F) :
    U.block Y n n (hilbertTensorInsert a (endpointWord d (fun _ : Fin n => r))) =
      hilbertTensorInsert (wordLevelRepeatedOperator T U Y n a)
        (endpointWord d (fun _ : Fin n => r)) := by
…

Mentions: OAI.KadisonSimilarity.SchurWeylMultilinearSpanning, OAI.KadisonSimilarity.normalizedPermutationContraction, OAI.KadisonSimilarity.hilbertTensorInsert, OAI.KadisonSimilarity.endpointWord, OAI.KadisonSimilarity.wordLevelRepeatedOperator

theorem OAI.KadisonSimilarity.wordLevelRepeatedOperator_apply line 95

Source documentation

Combining the two degree cases gives the actual ambient repeated-word action, with its canonical bounded multiplicity operator.

theorem wordLevelRepeatedOperator_apply
    (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 : ℕ) (a : G n) (d : E) (r : F) :
    Y (U.inclusion n (hilbertTensorInsert a (endpointWord d (fun _ : Fin n => r)))) =
      U.inclusion n (hilbertTensorInsert (wordLevelRepeatedOperator T U Y n a)
        (endpointWord d (fun _ : Fin n => r))) := by
…

theorem OAI.KadisonSimilarity.wordLevelRepeatedOperator_reference_independent line 119

Source documentation

Any normalized repeated tail gives the same compression, so the operator is independent of the reference unit letter used in its definition.

theorem wordLevelRepeatedOperator_reference_independent (n : ℕ)
    (spanning : ∀ s, SchurWeylMultilinearSpanning (Option (Fin n ⊕ Fin n)) (A s))
    (hcontraction : ∀ s (π : Equiv.Perm (Option (Fin n ⊕ Fin n))) v,
      normalizedPermutationContraction π (fun i => T.inclusion s (v i)) =
        normalizedPermutationContraction π v)
    (labels : ∀ s, Option (Fin n ⊕ Fin n) → A s)
    (hlabels : ∀ s, Function.Injective (labels s)) (r : F) (hr : ‖r‖ = 1) :
    multiplicityCompression (U.block Y n n)
      (endpointWord T.traceVector (fun _ : Fin n => r)) = wordLevelRepeatedOperator T U Y n :=
…

Mentions: OAI.KadisonSimilarity.SchurWeylMultilinearSpanning, OAI.KadisonSimilarity.normalizedPermutationContraction, OAI.KadisonSimilarity.multiplicityCompression, OAI.KadisonSimilarity.endpointWord, OAI.KadisonSimilarity.wordLevelRepeatedOperator

theorem OAI.KadisonSimilarity.adjoint_commutes_of_adjoint_commutes line 135
Source documentation
Commutation with an adjoint yields the required commutation for the adjoint of the ambient operator.
```
theorem adjoint_commutes_of_adjoint_commutes (Y Q : H →L[ℂ] H)
    (h : Y.comp Q.adjoint = Q.adjoint.comp Y) : Y.adjoint.comp Q = Q.comp Y.adjoint := by
…
```

theorem OAI.KadisonSimilarity.wordLevelRepeatedOperator_adjoint_apply line 143

Source documentation

Star closure of the actual global action families supplies the adjoint repeated-word action, with precisely the adjoint canonical multiplicity map.

theorem wordLevelRepeatedOperator_adjoint_apply
    (hleftStar : ∀ s a, (C.leftAction s a).adjoint = C.leftAction s (star a))
    (hunitaryStar : ∀ s u, (C.unitaryAction s u).adjoint = C.unitaryAction s u⁻¹)
    (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 : ℕ) (a : G n) (d : E) (r : F) :
    Y.adjoint (U.inclusion n (hilbertTensorInsert a (endpointWord d (fun _ : Fin n => r)))) =
      U.inclusion n (hilbertTensorInsert ((wordLevelRepeatedOperator T U Y n).adjoint a)
…