OAI/Analysis/KadisonSimilarity/FreeProduct/SourceConjugateFreeness.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonSimilarity.popa1995_concrete_inclusion line 36

   Source documentation

   The required specialization of Popa's conjugacy theorem for a concrete irreducible diffuse factor inclusion, with arbitrary smaller source algebra.

   theorem popa1995_concrete_inclusion
       [TopologicalSpace.SeparableSpace (vectorPositiveFunctional M υ.vector).GNS]
       (ω : Ultrafilter ℕ) (hω : (ω : Filter ℕ) ≤ Filter.cofinite)
       {D : Type*} [CStarAlgebra D] (ρ : D →⋆ₐ[ℂ] R.toStarSubalgebra) :
       Popa1995ConjugateFreenessInput (vectorPositiveFunctional R υ.vector)
         (vectorPositiveFunctional M υ.vector) (restrictedTrace υ hRM).trace_one υ.trace_one
         ω (restrictedTrace υ hRM).trace_mul_comm υ.trace_mul_comm
         (coordinateInclusion hRM) (fun _ => rfl) hω ρ := by
   …

   Mentions: OAI.KadisonSimilarity.vectorPositiveFunctional, OAI.KadisonSimilarity.Popa1995ConjugateFreenessInput