SemifiniteCornerStability.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Stability from a common countable matrix decomposition

Compression does not enlarge the distance, and the corner conjugacy inflates through the actual matrix units without enlarging its displacement. Only the initial corner is assumed to be a II₁ factor.

theorem OAI.KadisonKastler.FullMatrixCorner.spatial_of_common_entries line 27

Source documentation

The quantitative finite-factor estimate survives the common countable matrix decomposition, with exactly the same displacement bound.

theorem spatial_of_common_entries (h : FiniteFactorPublishedInputs.{u})
    (M N : VonNeumannAlgebra H)
    (hM : ∀ i j, F.entry i j ∈ M) (hN : ∀ i j, F.entry i j ∈ N)
    (hCorner : Generator.IsII1Factor
      (representedCorner E M (F.zero_zero ▸ hM 0 0)).toStarSubalgebra)
    {t : ℝ} (ht : 0 < t) (htEmbed : t < 1 / 100)
    (htPosition : 302 * t < 174 / 1000000000000000)
    (hgap : kkDistance M N < t)
    (htStandard : 3 * 50948 * Real.sqrt (302 * t) < 1 / 100000)
    (htSpatial : commonPositionError (302 * t) < 1 / 4000000) :
    ∃ v : unitary (H →L[ℂ] H), Conjugates v M N ∧
      ‖(v : H →L[ℂ] H) - 1‖ ≤ constructedFiniteFactorError t := by
…

Mentions: OAI.Generator.IsII1Factor, OAI.KadisonKastler.representedCorner, OAI.KadisonKastler.kkDistance, OAI.KadisonKastler.commonPositionError, OAI.KadisonKastler.Conjugates, OAI.KadisonKastler.constructedFiniteFactorError

theorem OAI.KadisonKastler.FullMatrixCorner.spatial_of_common_entries_right line 49

Source documentation

Either of the two initial corners may be the given II₁ factor.

theorem spatial_of_common_entries_right (h : FiniteFactorPublishedInputs.{u})
    (M N : VonNeumannAlgebra H)
    (hM : ∀ i j, F.entry i j ∈ M) (hN : ∀ i j, F.entry i j ∈ N)
    (hCorner : Generator.IsII1Factor
      (representedCorner E N (F.zero_zero ▸ hN 0 0)).toStarSubalgebra)
    {t : ℝ} (ht : 0 < t) (htEmbed : t < 1 / 100)
    (htPosition : 302 * t < 174 / 1000000000000000)
    (hgap : kkDistance M N < t)
    (htStandard : 3 * 50948 * Real.sqrt (302 * t) < 1 / 100000)
    (htSpatial : commonPositionError (302 * t) < 1 / 4000000) :
    ∃ v : unitary (H →L[ℂ] H), Conjugates v M N ∧
      ‖(v : H →L[ℂ] H) - 1‖ ≤ constructedFiniteFactorError t := by
…

theorem OAI.KadisonKastler.uniform_strong_stability_of_common_matrix_entries line 73

Source documentation

The same uniform tolerance as in the finite-factor theorem applies to all separably acting algebras with this common matrix decomposition.

theorem uniform_strong_stability_of_common_matrix_entries
    (h : FiniteFactorPublishedInputs.{u}) {ε : ℝ} (hε : 0 < ε) :
    ∃ δ : ℝ, 0 < δ ∧ ∀ (H : Type u) [NormedAddCommGroup H] [InnerProductSpace ℂ H]
      [CompleteSpace H] [TopologicalSpace.SeparableSpace H]
      (E : Submodule ℂ H) [CompleteSpace E] (F : FullMatrixCorner E)
      (M N : VonNeumannAlgebra H)
      (hM : ∀ i j, F.entry i j ∈ M) (_hN : ∀ i j, F.entry i j ∈ N),
      Generator.IsII1Factor
        (representedCorner E M (F.zero_zero ▸ hM 0 0)).toStarSubalgebra →
      kkDistance M N < δ → NearConjugacy M N ε := by
…

Mentions: OAI.KadisonKastler.FullMatrixCorner, OAI.Generator.IsII1Factor, OAI.KadisonKastler.representedCorner, OAI.KadisonKastler.kkDistance, OAI.KadisonKastler.NearConjugacy