TypeIMatrixPreparation.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Matrix preparation through the constructed type I algebra

Full countable matrix units generate an injective type I algebra directly. The finite signed groups in its actual matrix corners construct the small embedding directly. Neither the general amenable embedding nor the increasing-matrix injectivity input is needed for this step.

theorem OAI.KadisonKastler.exists_common_typeI_matrix_preparation line 28

Source documentation

The constructed embedding of the concrete matrix algebra makes its entries common.

theorem exists_common_typeI_matrix_preparation
    (M N : VonNeumannAlgebra H) (E : Submodule ℂ H) [CompleteSpace E]
    (F : FullMatrixCorner E) (hF : ∀ i j, F.entry i j ∈ M)
    {γ : ℝ} (hsmall : γ ≤ 1 / 1152) (hgap : kkDistance M N < γ) :
    ∃ a : unitary (H →L[ℂ] H),
      ‖(a : H →L[ℂ] H) - 1‖ ≤ 150 * γ ∧
      (∀ i j, F.entry i j ∈ unitaryConjugateAlgebra (star a) N) ∧
      kkDistance M (unitaryConjugateAlgebra (star a) N) < 301 * γ ∧
      MatrixNearInclusion M (unitaryConjugateAlgebra (star a) N) (301 * γ) ∧
      MatrixNearInclusion (unitaryConjugateAlgebra (star a) N) M (301 * γ) := by
…

Mentions: OAI.KadisonKastler.FullMatrixCorner, OAI.KadisonKastler.kkDistance, OAI.KadisonKastler.unitaryConjugateAlgebra, OAI.KadisonKastler.MatrixNearInclusion

theorem OAI.KadisonKastler.exists_typeIII_matrix_preparation_of_embedding line 47

Source documentation

Type III matrix preparation uses the constructed small embedding.

theorem exists_typeIII_matrix_preparation_of_embedding
    (M N : VonNeumannAlgebra H) (hM : TypeIIIFactor M)
    {γ : ℝ} (hsmall : γ ≤ 1 / 1152) (hgap : kkDistance M N < γ) :
    ∃ a : unitary (H →L[ℂ] H),
      ‖(a : H →L[ℂ] H) - 1‖ ≤ 150 * γ ∧
      kkDistance M (unitaryConjugateAlgebra (star a) N) < 301 * γ ∧
      MatrixNearInclusion M (unitaryConjugateAlgebra (star a) N) (301 * γ) ∧
      MatrixNearInclusion (unitaryConjugateAlgebra (star a) N) M (301 * γ) := by
…

Mentions: OAI.KadisonKastler.TypeIIIFactor, OAI.KadisonKastler.kkDistance, OAI.KadisonKastler.unitaryConjugateAlgebra, OAI.KadisonKastler.MatrixNearInclusion

theorem OAI.KadisonKastler.exists_properInfinite_matrix_preparation_of_embedding line 61

Source documentation

Every properly infinite identity has the same constructed matrix preparation.

theorem exists_properInfinite_matrix_preparation_of_embedding
    (M N : VonNeumannAlgebra H) (hM : ProperlyInfiniteIdentity M)
    {γ : ℝ} (hsmall : γ ≤ 1 / 1152) (hgap : kkDistance M N < γ) :
    ∃ a : unitary (H →L[ℂ] H),
      ‖(a : H →L[ℂ] H) - 1‖ ≤ 150 * γ ∧
      kkDistance M (unitaryConjugateAlgebra (star a) N) < 301 * γ ∧
      MatrixNearInclusion M (unitaryConjugateAlgebra (star a) N) (301 * γ) ∧
      MatrixNearInclusion (unitaryConjugateAlgebra (star a) N) M (301 * γ) := by
…

Mentions: OAI.KadisonKastler.ProperlyInfiniteIdentity, OAI.KadisonKastler.kkDistance, OAI.KadisonKastler.unitaryConjugateAlgebra, OAI.KadisonKastler.MatrixNearInclusion