OAI/Analysis/KadisonSimilarity/FreeProduct/TracialInclusionFreeness.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonSimilarity.TracialInclusionModel.exists_source_moments line 34
2. theorem OAI.KadisonSimilarity.popa1995_of_predual line 64

   Source documentation

   The source-unitary conclusion for a normal tracial inclusion with separable ambient predual. This is the specialization required by the matrix application.

   theorem popa1995_of_predual
       {X Y : Type u} [NormedAddCommGroup X] [NormedSpace ℂ X] [CompleteSpace X]
       [NormedAddCommGroup Y] [NormedSpace ℂ Y] [CompleteSpace Y]
       [TopologicalSpace.SeparableSpace Y]
       (eA : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] A) (eB : StrongDual ℂ Y ≃ₗᵢ⋆[ℂ] B)
       (τA : A →ₚ[ℂ] ℂ) (τB : B →ₚ[ℂ] ℂ)
       (hnA : BoundedHochschild.TraceInPredual eA τA)
       (hnB : BoundedHochschild.TraceInPredual eB τB)
       (h1A : τA 1 = 1) (h1B : τB 1 = 1)
       (trA : ∀ a b, τA (a * b) = τA (b * a))
       (trB : ∀ a b, τB (a * b) = τB (b * a))
       (hfB : ∀ a, τB (star a * a) = 0 → a = 0)
   …

   Mentions: OAI.BoundedHochschild.TraceInPredual