OAI/Analysis/KadisonSimilarity/FreeProduct/FreeWordHilbert.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonSimilarity.prod_pairWord line 17
2. theorem OAI.KadisonSimilarity.TracialCornerGeometry.trace_star line 33
3. theorem OAI.KadisonSimilarity.inner_tracialWordTensor line 44
4. theorem OAI.KadisonSimilarity.inner_reducedWord_eq_tensor line 70

   Source documentation

   Scalar freeness gives precisely the inner product of the actual tensors, including both unrestricted endpoint factors.

   theorem inner_reducedWord_eq_tensor (hτ : G.trace 1 = 1) (hf : ScalarFree G.trace D A)
       (n : ℕ) (d e : D) (b f : A) (a a' : Fin n → A) (c c' : Fin n → D)
       (ha : ∀ i, G.trace (a i : P) = 0) (ha' : ∀ i, G.trace (a' i : P) = 0)
       (hc : ∀ i, G.trace (c i : P) = 0) (hc' : ∀ i, G.trace (c' i : P) = 0) :
       inner ℂ (G.vector ((d : P) * alternatingProduct (fun i => (a i : P))
         (fun i => (c i : P)) * (b : P)))
         (G.vector ((e : P) * alternatingProduct (fun i => (a' i : P))
           (fun i => (c' i : P)) * (f : P))) =
         inner ℂ (tracialWordTensor G A D n d b a c ha hc)
           (tracialWordTensor G A D n e f a' c' ha' hc') := by
   …

   Mentions: OAI.KadisonSimilarity.ScalarFree, OAI.KadisonSimilarity.alternatingProduct, OAI.KadisonSimilarity.tracialWordTensor

5. theorem OAI.KadisonSimilarity.inner_reducedWord_ne line 93

   Source documentation

   Different numbers of centered pairs give orthogonal actual word vectors.

   theorem inner_reducedWord_ne (hτ : G.trace 1 = 1) (hf : ScalarFree G.trace D A)
       (n m : ℕ) (hnm : n ≠ m) (d e : D) (b f : A)
       (a : Fin n → A) (c : Fin n → D) (a' : Fin m → A) (c' : Fin m → D)
       (ha : ∀ i, G.trace (a i : P) = 0) (ha' : ∀ i, G.trace (a' i : P) = 0)
       (hc : ∀ i, G.trace (c i : P) = 0) (hc' : ∀ i, G.trace (c' i : P) = 0) :
       inner ℂ (G.vector ((d : P) * alternatingProduct (fun i => (a i : P))
         (fun i => (c i : P)) * (b : P)))
         (G.vector ((e : P) * alternatingProduct (fun i => (a' i : P))
           (fun i => (c' i : P)) * (f : P))) = 0 := by
   …

   Mentions: OAI.KadisonSimilarity.ScalarFree, OAI.KadisonSimilarity.alternatingProduct