LocalizedMatrixChainEmbedding.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Localized embedding of an increasing matrix closure

theorem OAI.KadisonKastler.exists_unitary_embedding_of_invariant_group_in_algebra line 17

Source documentation

A generating representation gives an embedding of the whole algebra, with the unitary retained inside any prescribed containing algebra.

theorem exists_unitary_embedding_of_invariant_group_in_algebra
    (m : ScalarInvariantMean G) {M N J : VonNeumannAlgebra H}
    (hMJ : M ≤ J) (hNJ : N ≤ J) (U : G →* unitary (Algebra M))
    (hgen : generatedVonNeumannAlgebra
      (StarAlgebra.adjoin ℂ (Set.range (fun g => (U g : H →L[ℂ] H)))) = M)
    {γ : ℝ} (hγ : 0 ≤ γ) (hsmall : γ ≤ 1 / 1152) (hnear : NearInclusion M N γ) :
    ∃ w : unitary (H →L[ℂ] H), (w : H →L[ℂ] H) ∈ J ∧
      (∀ x ∈ M, unitaryConj w x ∈ N) ∧ ‖(w : H →L[ℂ] H) - 1‖ ≤ 84 * γ := by
…

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

theorem OAI.KadisonKastler.exists_unitary_matrixChain_embedding_in_algebra line 47

Source documentation

Localized embedding for the actual increasing full-matrix closure.

theorem exists_unitary_matrixChain_embedding_in_algebra [Nontrivial H]
    {A : ℕ → StarSubalgebra ℂ (H →L[ℂ] H)}
    (F : ∀ n, FullMatrixFrame (A n)) (hA : Monotone A)
    {N J : VonNeumannAlgebra H}
    (hRJ : generatedVonNeumannAlgebra (⨆ n, A n) ≤ J) (hNJ : N ≤ J)
    {γ : ℝ} (hγ : 0 ≤ γ) (hsmall : γ ≤ 1 / 1152)
    (hnear : NearInclusion (generatedVonNeumannAlgebra (⨆ n, A n)) N γ) :
    ∃ w : unitary (H →L[ℂ] H), (w : H →L[ℂ] H) ∈ J ∧
      (∀ x ∈ generatedVonNeumannAlgebra (⨆ n, A n), unitaryConj w x ∈ N) ∧
      ‖(w : H →L[ℂ] H) - 1‖ ≤ 84 * γ := by
…

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

theorem OAI.KadisonKastler.exists_localized_unitary_matrixChain_embedding line 71

Source documentation

The conjugating unitary belongs to the algebra generated by the source matrix closure and its nearby target.

theorem exists_localized_unitary_matrixChain_embedding [Nontrivial H]
    {A : ℕ → StarSubalgebra ℂ (H →L[ℂ] H)}
    (F : ∀ n, FullMatrixFrame (A n)) (hA : Monotone A)
    {N : VonNeumannAlgebra H} {γ : ℝ} (hγ : 0 ≤ γ) (hsmall : γ ≤ 1 / 1152)
    (hnear : NearInclusion (generatedVonNeumannAlgebra (⨆ n, A n)) N γ) :
    ∃ w : unitary (H →L[ℂ] H),
      (w : H →L[ℂ] H) ∈ generatedVonNeumannAlgebra
        ((generatedVonNeumannAlgebra (⨆ n, A n)).toStarSubalgebra ⊔ N.toStarSubalgebra) ∧
      (∀ x ∈ generatedVonNeumannAlgebra (⨆ n, A n), unitaryConj w x ∈ N) ∧
      ‖(w : H →L[ℂ] H) - 1‖ ≤ 84 * γ := by
…

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