CompleteWeakLimits.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Completely bounded maps into a concrete von Neumann algebra have weak ultralimits.

theorem OAI.KadisonKastler.completelyBoundedBy_of_weak_operator_ultralimit line 26

theorem OAI.KadisonKastler.exists_completelyBounded_weak_ultralimit line 45

Source documentation

Pointwise weak compactness preserves the full matrix norm bound.

theorem exists_completelyBounded_weak_ultralimit (M : VonNeumannAlgebra H)
    {ι : Type*} (ω : Ultrafilter ι) (F : ι → Algebra M →ₗ[ℂ] Algebra M)
    {c : ℝ} (hc : 0 ≤ c) (hF : ∀ i, CompletelyBoundedBy (F i) c) :
    ∃ L : Algebra M →ₗ[ℂ] Algebra M, CompletelyBoundedBy L c ∧
      ∀ a ξ η, Tendsto (fun i => inner ℂ η ((F i a : H →L[ℂ] H) ξ))
        (ω : Filter ι) (𝓝 (inner ℂ η ((L a : H →L[ℂ] H) ξ))) := by
…

Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.CompletelyBoundedBy