DihedralWordColumn.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The actual normalized dihedral columns agree with the repeated tensor words on the dense bounded algebra vectors.

theorem OAI.KadisonSimilarity.TracialCornerGeometry.baseSymmetryRepeatedInclusion_baseVector line 39
Source documentation
The repeated base insertion is the bounded-algebra multiplicity word.
```
theorem baseSymmetryRepeatedInclusion_baseVector (k : ℕ) (b : A) :
    G.baseSymmetryRepeatedInclusion A s hs0 hsstar hssq hτ k (G.baseVector A b) =
      tracialMultiplicityWord G A k b (fun _ => s) (fun _ => hs0) := rfl
```
Mentions: OAI.KadisonSimilarity.tracialMultiplicityWord

theorem OAI.KadisonSimilarity.TracialCornerGeometry.repeated_dihedral_word_formula line 45

Source documentation

A constant-letter word has exactly the tensor coordinates of the repeated base insertion and the unnormalized endpoint.

theorem repeated_dihedral_word_formula (hU : TracialWordFormula G A D U)
    (k : ℕ) (b : A) :
    U.inclusion k
      (hilbertTensorInsert
        (G.baseSymmetryRepeatedInclusion A s hs0 hsstar hssq hτ k (G.baseVector A b))
        (tracialEndpointWord G D k e (fun _ => d) (fun _ => hd0))) =
      G.vector ((e : P) * ((s : P) * (d : P)) ^ k * (b : P)) := by
…

Mentions: OAI.KadisonSimilarity.TracialWordFormula, OAI.KadisonSimilarity.hilbertTensorInsert, OAI.KadisonSimilarity.tracialEndpointWord

theorem OAI.KadisonSimilarity.TracialCornerGeometry.actual_dihedral_column_baseVector line 57

Source documentation

The two column realizations agree on all bounded algebra vectors.

theorem actual_dihedral_column_baseVector (hf : ScalarFree G.trace D A)
    (hU : TracialWordFormula G A D U) (k : ℕ) (b : A) :
    G.tracialDihedralInclusion D A hf hτ d s e hdstar hdsq hd0 hsstar hssq hs0
      he ht hte k (G.baseVector A b) =
      dihedralNormalization t • U.inclusion k (hilbertTensorInsert
        (G.baseSymmetryRepeatedInclusion A s hs0 hsstar hssq hτ k (G.baseVector A b))
        (tracialEndpointWord G D k e (fun _ => d) (fun _ => hd0))) := by
…

Mentions: OAI.KadisonSimilarity.ScalarFree, OAI.KadisonSimilarity.TracialWordFormula, OAI.KadisonSimilarity.dihedralNormalization, OAI.KadisonSimilarity.hilbertTensorInsert, OAI.KadisonSimilarity.tracialEndpointWord