FiniteStageEmbedding.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Embeddings for the matrix stages used by the stability proof

theorem OAI.KadisonKastler.matrixUnits_index_nonempty line 18

Source documentation

A nonzero full matrix representation has a nonempty index set.

theorem matrixUnits_index_nonempty {ι : Type*} [Fintype ι] [DecidableEq ι]
    (E : MatrixUnitSystem ι (H →L[ℂ] H)) : Nonempty ι := by
…

theorem OAI.KadisonKastler.exists_localized_unitary_matrixUnits_embedding line 26

Source documentation

The concrete matrix-unit formulation needs no injectivity or embedding input.

theorem exists_localized_unitary_matrixUnits_embedding
    (s : ℕ → ℕ) (E : ∀ n, MatrixUnitSystem (Fin (s n)) (H →L[ℂ] H))
    (hmono : Monotone (fun n => (E n).algebra))
    {R N : VonNeumannAlgebra H}
    (hR : R = generatedVonNeumannAlgebra (⨆ n, (E n).algebra))
    {γ : ℝ} (hγ : 0 ≤ γ) (hsmall : γ ≤ 1 / 1152) (hnear : NearInclusion R N γ) :
    ∃ w : unitary (H →L[ℂ] H),
      (w : H →L[ℂ] H) ∈ generatedVonNeumannAlgebra (R.toStarSubalgebra ⊔ N.toStarSubalgebra) ∧
      (∀ x ∈ R, unitaryConj w x ∈ N) ∧ ‖(w : H →L[ℂ] H) - 1‖ ≤ 84 * γ := by
…

Mentions: OAI.KadisonKastler.generatedVonNeumannAlgebra, OAI.KadisonKastler.NearInclusion, OAI.KadisonKastler.unitaryConj

theorem OAI.KadisonKastler.exists_localized_unitary_finiteStage_embedding line 42

Source documentation

The finite-stage formulation preserves the actual source algebra and the location in the join with the target.

theorem exists_localized_unitary_finiteStage_embedding
    {M N : VonNeumannAlgebra H} (A : ℕ → FiniteMatrixStage M)
    (hA : Monotone (fun n => (A n).units.concreteAlgebra))
    {γ : ℝ} (hγ : 0 ≤ γ) (hsmall : γ ≤ 1 / 1152)
    (hnear : NearInclusion (FiniteMatrixStage.generatedVonNeumann A) N γ) :
    ∃ w : unitary (H →L[ℂ] H),
      (w : H →L[ℂ] H) ∈ generatedVonNeumannAlgebra
        ((FiniteMatrixStage.generatedVonNeumann A).toStarSubalgebra ⊔ N.toStarSubalgebra) ∧
      (∀ x ∈ FiniteMatrixStage.generatedVonNeumann A, unitaryConj w x ∈ N) ∧
      ‖(w : H →L[ℂ] H) - 1‖ ≤ 84 * γ :=
…

Mentions: OAI.KadisonKastler.NearInclusion, OAI.KadisonKastler.generatedVonNeumannAlgebra, OAI.KadisonKastler.unitaryConj

theorem OAI.KadisonKastler.exists_common_matrixStage_neighbor_of_kkDistance_lt line 58

Source documentation

Put the actual increasing matrix closure into common position. The existing downstream constants are retained.

theorem exists_common_matrixStage_neighbor_of_kkDistance_lt
    {M N : VonNeumannAlgebra H} (A : ℕ → FiniteMatrixStage M)
    (hA : Monotone (fun n => (A n).units.concreteAlgebra))
    {t : ℝ} (ht : 0 ≤ t) (hsmall : t ≤ 1 / 1152) (hgap : kkDistance M N < t) :
    ∃ w : unitary (H →L[ℂ] H),
      FiniteMatrixStage.generatedVonNeumann A ≤ unitaryConjugateAlgebra (star w) N ∧
      ‖(w : H →L[ℂ] H) - 1‖ ≤ 150 * t ∧
      kkDistance M (unitaryConjugateAlgebra (star w) N) ≤
        kkDistance M N + 2 * ‖(w : H →L[ℂ] H) - 1‖ := by
…

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