AmenableMatrixStability.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Removing the common matrix-unit hypothesis

A countable full matrix corner in an injective subalgebra is moved into the neighbor using the constructed finite-group embedding. The original finite corner and its representation remain fixed throughout this step.

def OAI.KadisonKastler.matrixCornerError line 24
Source documentation
The displacement from the injective embedding followed by the finite corner conjugacy.
```
def matrixCornerError (t : ℝ) : ℝ := 150 * t + constructedFiniteFactorError (302 * t)
```
Mentions: OAI.KadisonKastler.constructedFiniteFactorError
theorem OAI.KadisonKastler.continuous_matrixCornerError line 26
theorem OAI.KadisonKastler.matrixCornerError_zero line 31
theorem OAI.KadisonKastler.matrixCornerError_monotone line 34

theorem OAI.KadisonKastler.FullMatrixCorner.spatial_of_injective_matrix_subalgebra line 50

Source documentation

A nearby algebra need not already contain the matrix units. The constructed matrix embedding creates this common position, after which compression and the proved inflation theorem provide the whole-space conjugacy.

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

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

theorem OAI.KadisonKastler.uniform_strong_stability_of_injective_matrix_subalgebra line 80

Source documentation

Uniform strong stability when the source has an injective matrix subalgebra with a finite-factor initial corner. The matrix subalgebra is not required to lie in the neighbor.

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

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