TracialWordDensity.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Equality of bounded word maps can be tested on actual bounded algebra letters. This bridges the published product formula to completed word actions.

theorem OAI.KadisonSimilarity.TracialCornerGeometry.continuousLinearMap_ext_tracialWordTensors line 40

Source documentation

Bounded algebra vectors determine every continuous map on a word level.

theorem continuousLinearMap_ext_tracialWordTensors (hτ : G.trace 1 = 1) (n : ℕ)
    (f g : HilbertTensor
      (HilbertTensor (CompletedTensorWord (centeredSubspace (G.baseVector A 1)) n)
        (G.baseSpace A))
      (EndpointTensor (G.baseSpace D) (centeredSubspace (G.baseVector D 1)) n) →L[ℂ] K)
    (h : ∀ (d : D) (b : A) (a : Fin n → A) (c : Fin n → D)
      (ha : ∀ i, G.trace (a i : P) = 0) (hc : ∀ i, G.trace (c i : P) = 0),
      f (tracialWordTensor G A D n d b a c ha hc) =
        g (tracialWordTensor G A D n d b a c ha hc)) : f = g := by
…

Mentions: OAI.KadisonSimilarity.HilbertTensor, OAI.KadisonSimilarity.CompletedTensorWord, OAI.KadisonSimilarity.centeredSubspace, OAI.KadisonSimilarity.EndpointTensor, OAI.KadisonSimilarity.tracialWordTensor

theorem OAI.KadisonSimilarity.TracialCornerGeometry.function_ext_tracialWordTensors line 64

Source documentation

Equality on bounded algebra words determines a continuous map on the completed word space.

theorem function_ext_tracialWordTensors (hτ : G.trace 1 = 1) (n : ℕ)
    (p q : HilbertTensor
      (HilbertTensor (CompletedTensorWord (centeredSubspace (G.baseVector A 1)) n)
        (G.baseSpace A))
      (EndpointTensor (G.baseSpace D) (centeredSubspace (G.baseVector D 1)) n) → K)
    (hp : Continuous p) (hq : Continuous q)
    (hpadd : ∀ x y, p (x + y) = p x + p y) (hqadd : ∀ x y, q (x + y) = q x + q y)
    (hpsmul : ∀ (c : ℂ) x, p (c • x) = c • p x)
    (hqsmul : ∀ (c : ℂ) x, q (c • x) = c • q x)
    (h : ∀ (d : D) (b : A) (a : Fin n → A) (c : Fin n → D)
      (ha : ∀ i, G.trace (a i : P) = 0) (hc : ∀ i, G.trace (c i : P) = 0),
      p (tracialWordTensor G A D n d b a c ha hc) =
…