OAI/Analysis/KadisonSimilarity/Tracial/SourceUnitaryMoments.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonSimilarity.exists_source_unitary_small_moments line 27

   Source documentation

   A unitary in the source makes any finite family of centered ambient mixed moments arbitrarily small.

   theorem exists_source_unitary_small_moments {I : Type*} [Fintype I]
       (F : I → M.toStarSubalgebra)
       (hF : ∀ i, ‖F i‖ ≤ 1) (hFτ : ∀ i, υ.trace (F i) = 0)
       {K N : ℕ} (hK : 0 < K) {ε : ℝ} (hε : 0 < ε) :
       ∃ u : unitary R.toStarSubalgebra, ∀ a : BoundedWord I K N,
         admissibleTail a.2.val →
           ‖υ.trace (mixedEval F (SourcePartialUnitary.map (coordinateInclusion hRM)
             (asPartialUnitary u)) a.1 a.2.val)‖ < ε := by
   …

   Mentions: OAI.KadisonSimilarity.SourcePartialUnitary.map