OAI/Analysis/KadisonSimilarity/FreeProduct/FreePairWords.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.KadisonSimilarity.CenteredPairWord line 15

   Source documentation

   A sequence of centered A,D pairs, including the empty sequence.

   inductive CenteredPairWord (τ : R →ₗ[ℂ] ℂ) (A D : StarSubalgebra ℂ R) : List R → Prop
     | nil : CenteredPairWord τ A D []
     | cons {a d : R} {xs : List R} (ha : a ∈ A) (hd : d ∈ D)
         (ha0 : τ a = 0) (hd0 : τ d = 0) (hxs : CenteredPairWord τ A D xs) :
         CenteredPairWord τ A D (a :: d :: xs)
   
   namespace CenteredPairWord

2. theorem OAI.KadisonSimilarity.CenteredPairWord.alternating line 23
3. theorem OAI.KadisonSimilarity.CenteredPairWord.alternating_append line 30
4. theorem OAI.KadisonSimilarity.CenteredPairWord.even_length line 38
5. theorem OAI.KadisonSimilarity.ScalarFree.trace_pairWords_right_centered line 48
6. theorem OAI.KadisonSimilarity.ScalarFree.trace_pairWords_centered_middle line 62
7. theorem OAI.KadisonSimilarity.ScalarFree.trace_pairWords_endpoints line 83

   Source documentation

   Full endpoints factor off from the inner product of centered pair words.

   theorem ScalarFree.trace_pairWords_endpoints (hf : ScalarFree τ A D)
       (hstar : ∀ x, τ (star x) = star (τ x)) (hτ : τ 1 = 1)
       {xs ys : List R} (hxs : CenteredPairWord τ A D xs)
       (hys : CenteredPairWord τ A D ys) {q r : R} (hq : q ∈ D) (hr : r ∈ A) :
       τ (star xs.prod * q * ys.prod * r) =
         τ q * τ r * centeredWordPairing τ xs ys := by
   …

   Mentions: OAI.KadisonSimilarity.ScalarFree, OAI.KadisonSimilarity.CenteredPairWord, OAI.KadisonSimilarity.centeredWordPairing

8. def OAI.KadisonSimilarity.pairWord line 111

   Source documentation

   Interleave two equally long lists of letters in their original order.

   def pairWord : {n : ℕ} → (Fin n → R) → (Fin n → R) → List R
     | 0, _, _ => []
     | _ + 1, a, d => a 0 :: d 0 :: pairWord (Fin.tail a) (Fin.tail d)
   
   omit [Ring R] [Algebra ℂ R] [StarRing R] [StarModule ℂ R] in

9. theorem OAI.KadisonSimilarity.length_pairWord line 116
10. theorem OAI.KadisonSimilarity.CenteredPairWord.of_pairWord line 122
11. theorem OAI.KadisonSimilarity.centeredWordPairing_pairWord line 134
12. theorem OAI.KadisonSimilarity.ScalarFree.trace_full_pairWords line 144

    Source documentation

    The actual trace inner product of words with unrestricted endpoints.

    theorem ScalarFree.trace_full_pairWords (hf : ScalarFree τ A D)
        (hstar : ∀ x, τ (star x) = star (τ x)) (hτ : τ 1 = 1)
        (htr : ∀ x y, τ (x * y) = τ (y * x))
        {xs ys : List R} (hxs : CenteredPairWord τ A D xs)
        (hys : CenteredPairWord τ A D ys) {d e b c : R}
        (hd : d ∈ D) (he : e ∈ D) (hb : b ∈ A) (hc : c ∈ A) :
        τ (star (d * xs.prod * b) * (e * ys.prod * c)) =
          τ (star d * e) * τ (star b * c) * centeredWordPairing τ xs ys := by
    …

    Mentions: OAI.KadisonSimilarity.ScalarFree, OAI.KadisonSimilarity.CenteredPairWord, OAI.KadisonSimilarity.centeredWordPairing