ReducedWordModel.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

The reduced-word part of the published free-product construction.

Ricard–Xu, J. reine angew. Math. 599 (2006), Section 1, pp. 2–3 of arXiv:math/0505302, constructs the reduced free-product Hilbert space as the orthogonal sum of alternating centered tensor words. Regrouping the first and last factors gives the coordinates below. The input is only this word construction, without any operator invariance or commutator estimate.

def OAI.KadisonSimilarity.alternatingProduct line 22
Source documentation
The finite alternating product, in its prescribed left-to-right order.
```
def alternatingProduct {n : ℕ} (a b : Fin n → P) : P :=
…
```
theorem OAI.KadisonSimilarity.alternatingProduct_zero line 25
theorem OAI.KadisonSimilarity.alternatingProduct_constant line 28
def OAI.KadisonSimilarity.reducedWordVectors line 36
Source documentation
The actual alternating vectors whose span is dense in a reduced product.
```
def reducedWordVectors : Set H := {x | ∃ (n : ℕ) (d : D) (b : A)
…
```
def OAI.KadisonSimilarity.ReducedWordGenerated line 44
Source documentation
Being generated in the tracial Hilbert space is a density hypothesis, not an operator conclusion.
```
def ReducedWordGenerated : Prop :=
…
```
def OAI.KadisonSimilarity.tracialMultiplicityWord line 48
Source documentation
The base-algebra part of an elementary word.
```
def tracialMultiplicityWord (n : ℕ) (b : A) (a : Fin n → A)
    (ha : ∀ i, G.trace (a i : P) = 0) : WordMultiplicity (G.baseVector A 1) n :=
…
```
Mentions: OAI.KadisonSimilarity.WordMultiplicity
def OAI.KadisonSimilarity.tracialEndpointWord line 54
Source documentation
The other-factor endpoint and centered internal letters.
```
def tracialEndpointWord (n : ℕ) (d : D) (c : Fin n → D)
    (hc : ∀ i, G.trace (c i : P) = 0) :
    EndpointTensor (G.baseSpace D) (centeredSubspace (G.baseVector D 1)) n :=
…
```
Mentions: OAI.KadisonSimilarity.EndpointTensor, OAI.KadisonSimilarity.centeredSubspace

def OAI.KadisonSimilarity.tracialWordTensor line 60

Source documentation

The tensor product of the base-word and endpoint factors.

def tracialWordTensor (n : ℕ) (d : D) (b : A) (a : Fin n → A) (c : Fin n → D)
    (ha : ∀ i, G.trace (a i : P) = 0) (hc : ∀ i, G.trace (c i : P) = 0) :
    MultiplicityWordSpace (WordMultiplicity (G.baseVector A 1)) (G.baseSpace D)
      (centeredSubspace (G.baseVector D 1)) n :=
…

Mentions: OAI.KadisonSimilarity.MultiplicityWordSpace, OAI.KadisonSimilarity.WordMultiplicity, OAI.KadisonSimilarity.centeredSubspace

def OAI.KadisonSimilarity.TracialWordFormula line 68
Source documentation
Regrouped ordinary free-product words. The multiplicity space and the endpoint space are fixed concrete tensor products of the two base spaces.
```
def TracialWordFormula (U : OrthogonalWordLevels
    (MultiplicityWordSpace (WordMultiplicity (G.baseVector A 1)) (G.baseSpace D)
      (centeredSubspace (G.baseVector D 1))) H) : Prop :=
…
```
Mentions: OAI.KadisonSimilarity.OrthogonalWordLevels, OAI.KadisonSimilarity.MultiplicityWordSpace, OAI.KadisonSimilarity.WordMultiplicity, OAI.KadisonSimilarity.centeredSubspace
def OAI.KadisonSimilarity.RicardXuWordDecompositionInput line 79
Source documentation
Published input: the alternating centered tensor model for a normalized faithful tracial reduced product. Its only output is the word coordinates.
```
def RicardXuWordDecompositionInput : Prop :=
…
```

theorem OAI.KadisonSimilarity.TracialWordFormula.repeated_word_formula line 96

Source documentation

Constant centered letters recover the exact repeated-word formula.

theorem repeated_word_formula (n : ℕ) (d₀ d : D) (a b : A)
    (ha : G.trace (a : P) = 0) (hd : G.trace (d : P) = 0) :
    U.inclusion n (tracialWordTensor G A D n d₀ b
      (fun _ => a) (fun _ => d) (fun _ => ha) (fun _ => hd)) =
      G.vector ((d₀ : P) * ((a : P) * (d : P)) ^ n * (b : P)) := by
…

Mentions: OAI.KadisonSimilarity.tracialWordTensor

theorem OAI.KadisonSimilarity.TracialWordFormula.zero_word_formula line 105

Source documentation

Degree zero is the actual product of a head vector and a base vector.

theorem zero_word_formula (d : D) (b : A) :
    U.inclusion 0 (tracialWordTensor G A D 0 d b Fin.elim0 Fin.elim0
      (fun i => Fin.elim0 i) (fun i => Fin.elim0 i)) =
      G.vector ((d : P) * (b : P)) := by
…

Mentions: OAI.KadisonSimilarity.tracialWordTensor