OAI/Analysis/KadisonKastler/LocalizedGroupEmbedding.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Localized simultaneous group embeddings

Performing the final intertwining average and polar decomposition inside a specified von Neumann algebra retains the location of the conjugating unitary.

  1. theorem OAI.KadisonKastler.exists_unitary_invariantGroup_embedding_in_algebra line 22

    Source documentation

    The embedding unitary lies in any ambient von Neumann algebra containing both the original and the target algebra.

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

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