ConstructedMatrixFactorStability.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Finite-factor stability with constructed matrix embeddings

Increasing matrix stages give the initial common position for the nearby finite factors.

theorem OAI.KadisonKastler.constructed_finiteFactor_spatial_of_matrixStages line 40

Source documentation

Common tracial position, boundary means and field projections give a small unitary conjugacy for the finite factors.

theorem constructed_finiteFactor_spatial_of_matrixStages
    (hPosition : PublishedCommonTracialPosition.{u})
    (hBoundary : PublishedBoundary.{u})
    (hTom : ∀ (K : Type u) [NormedAddCommGroup K] [InnerProductSpace ℂ K]
      [CompleteSpace K] [TopologicalSpace.SeparableSpace K], PublishedFieldTomiyamaFamily K)
    (hM : Generator.IsII1Factor M.toStarSubalgebra)
    (hN : Generator.IsII1Factor N.toStarSubalgebra)
    (A : ℕ → Generator.FiniteMatrixStage M)
    (hA : Monotone (fun n => (A n).units.concreteAlgebra))
    (hirr : ∀ a : Algebra M,
      (∀ r : Algebra (Generator.FiniteMatrixStage.generatedVonNeumann A),
        coordinateInclusion (Generator.FiniteMatrixStage.generatedVonNeumann_le A) r * a =
…

Mentions: OAI.KadisonKastler.PublishedFieldTomiyamaFamily, OAI.Generator.IsII1Factor, OAI.Generator.FiniteMatrixStage, OAI.KadisonKastler.Algebra, OAI.Generator.FiniteMatrixStage.generatedVonNeumann, OAI.Generator.FiniteMatrixStage.generatedVonNeumann_le