OAI/Analysis/KadisonSimilarity/Tracial/SourcePartialUnitaries.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Partial unitaries remain in the source while their moments are evaluated in the ambient algebra.

  1. def OAI.KadisonSimilarity.SourcePartialUnitary.map line 20

    Source documentation

    Apply the given inclusion to a partial unitary.

    def map (φ : A →⋆ₐ[ℂ] B) (v : PartialUnitary A) : PartialUnitary B :=
…
  2. theorem OAI.KadisonSimilarity.SourcePartialUnitary.coe_map line 27
  3. theorem OAI.KadisonSimilarity.SourcePartialUnitary.support_map line 30
  4. theorem OAI.KadisonSimilarity.SourcePartialUnitary.map_zero line 35
  5. theorem OAI.KadisonSimilarity.SourcePartialUnitary.power_map line 38
  6. theorem OAI.KadisonSimilarity.SourcePartialUnitary.map_orthogonalSum line 43
  7. theorem OAI.KadisonSimilarity.source_gns_tendsto line 56

    Source documentation

    Source trace-norm convergence is exactly convergence after inclusion.

    theorem source_gns_tendsto {J : Type*} {l : Filter J}
    {a : J → N.toStarSubalgebra} {b : N.toStarSubalgebra}
    (h : GNSTendsto (vectorPositiveFunctional N υ.vector) a l b) :
    GNSTendsto (vectorPositiveFunctional M υ.vector)
      (fun j => coordinateInclusion hNM (a j)) l (coordinateInclusion hNM b) := by
…

    Mentions: OAI.KadisonSimilarity.vectorPositiveFunctional