OAI/Analysis/KadisonKastler/FullCornerPreparation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Putting countable matrix entries in common position

  1. theorem OAI.KadisonKastler.FullMatrixCorner.exists_common_neighbor line 18

    Source documentation

    The constructed finite-group embedding makes all countable matrix entries common and retains the elementary displacement and gap estimates.

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

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