OAI/Analysis/KadisonSimilarity/FreeProduct/FreeWordInnerProducts.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Inner-product recursion for reduced words. Freeness alone supplies orthogonality at different first factors and contraction of matching first letters. These are the algebraic identities needed for the tensor model.

  1. theorem OAI.KadisonSimilarity.star_list_prod line 16
  2. theorem OAI.KadisonSimilarity.AlternatingCenteredWord.star_reverse_append line 22
  3. theorem OAI.KadisonSimilarity.ScalarFree.trace_of_nonempty line 38
  4. theorem OAI.KadisonSimilarity.ScalarFree.trace_opposite_words line 45
  5. theorem OAI.KadisonSimilarity.ScalarFree.trace_centered_sandwich line 59
  6. theorem OAI.KadisonSimilarity.ScalarFree.trace_matching_heads line 71
  7. def OAI.KadisonSimilarity.centeredWordPairing line 101

    Source documentation

    The scalar product of two equally oriented centered words. Unequal lengths give zero, including a nonempty word paired with the vacuum.

    def centeredWordPairing (τ : R →ₗ[ℂ] ℂ) : List R → List R → ℂ
  | [], [] => 1
  | a :: xs, b :: ys => τ (star a * b) * centeredWordPairing τ xs ys
  | _, _ => 0
  8. theorem OAI.KadisonSimilarity.ScalarFree.trace_same_words line 106
  9. theorem OAI.KadisonSimilarity.centeredWordPairing_eq_zero_of_length_ne line 131
  10. theorem OAI.KadisonSimilarity.ScalarFree.trace_words_of_length_ne line 145
  11. theorem OAI.KadisonSimilarity.centeredWordPairing_ofFn line 154
  12. theorem OAI.KadisonSimilarity.ScalarFree.trace_words_ofFn line 162