OAI/Analysis/KadisonKastler/MatrixVectorTrace.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.inner_tupleSingle_hilbertMatrix line 23
2. theorem OAI.KadisonKastler.matrixTrace_vector_formula line 33

   Source documentation

   A finite vector formula for the base trace gives one for the matrix trace, by placing each vector in each coordinate of the direct sum.

   theorem matrixTrace_vector_formula (τ : FaithfulTracialState B)
       (ρ : B →⋆ₐ[ℂ] (H →L[ℂ] H)) {k : ℕ} (ξ η : Fin k → H)
       (hτ : ∀ b, τ.toLinearMap b = ∑ a, inner ℂ (η a) (ρ b (ξ a)))
       (x : CStarMatrix ι ι B) :
       (matrixTrace τ).toLinearMap x =
         ∑ i : ι, ∑ a : Fin k,
           inner ℂ (Generator.tupleSingle i (η a))
             (hilbertMatrix (x.map ρ)
               (((((Fintype.card ι : ℝ)⁻¹ : ℝ) : ℂ)) • Generator.tupleSingle i (ξ a))) := by
   …

   Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.matrixTrace, OAI.Generator.tupleSingle, OAI.KadisonKastler.hilbertMatrix

3. theorem OAI.KadisonKastler.matrixTrace_finiteVector_formula line 45