OAI/Analysis/KadisonSimilarity/FreeProduct/TracialWordIsometry.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Construction of the completed free-product word inclusions from the proved Gram identities and totality of elementary tensors.

  1. abbrev OAI.KadisonSimilarity.CenteredTracialLetter line 20
  2. def OAI.KadisonSimilarity.centeredLetterVector line 22
  3. theorem OAI.KadisonSimilarity.centeredLetterVector_dense line 25
  4. abbrev OAI.KadisonSimilarity.TracialWordParameter line 41
  5. def OAI.KadisonSimilarity.tracialTensorFamily line 45
  6. def OAI.KadisonSimilarity.tracialAlgebraFamily line 49
  7. theorem OAI.KadisonSimilarity.tracialTensorFamily_dense line 53
  8. theorem OAI.KadisonSimilarity.tracialFamilyGram line 64
  9. def OAI.KadisonSimilarity.tracialWordInclusion line 75

    Source documentation

    The genuine isometric inclusion of one completed word level.

    def tracialWordInclusion (hτ : G.trace 1 = 1) (hf : ScalarFree G.trace D A) (n : ℕ) :
    MultiplicityWordSpace (WordMultiplicity (G.baseVector A 1)) (G.baseSpace D)
      (centeredSubspace (G.baseVector D 1)) n →ₗᵢ[ℂ] H :=
…

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

  10. theorem OAI.KadisonSimilarity.tracialWordInclusion_family line 81
  11. theorem OAI.KadisonSimilarity.tracialWordInclusion_orthogonal line 90
  12. theorem OAI.KadisonSimilarity.tracialWordInclusion_dense_span line 122
  13. def OAI.KadisonSimilarity.tracialOrthogonalWordLevels line 138

    Source documentation

    The completed orthogonal word decomposition, built from freeness.

    def tracialOrthogonalWordLevels (hτ : G.trace 1 = 1)
    (hf : ScalarFree G.trace D A) (hgen : ReducedWordGenerated G A D) :
    OrthogonalWordLevels
      (MultiplicityWordSpace (WordMultiplicity (G.baseVector A 1)) (G.baseSpace D)
        (centeredSubspace (G.baseVector D 1))) H where
…

    Mentions: OAI.KadisonSimilarity.ScalarFree, OAI.KadisonSimilarity.ReducedWordGenerated, OAI.KadisonSimilarity.OrthogonalWordLevels, OAI.KadisonSimilarity.MultiplicityWordSpace, OAI.KadisonSimilarity.WordMultiplicity, OAI.KadisonSimilarity.centeredSubspace

  14. theorem OAI.KadisonSimilarity.ricardXuWordDecompositionInput line 148

    Source documentation

    Ricard--Xu's regrouped word coordinates follow from tracial freeness.

    theorem ricardXuWordDecompositionInput : RicardXuWordDecompositionInput G A D := by
…

    Mentions: OAI.KadisonSimilarity.RicardXuWordDecompositionInput