ContractiveWeakLimit.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Contractive weak limits with a faithful trace vector

Pointwise weak compactness constructs a contractive ambient map. Strong convergence on the given separating trace vector suffices to prove that its restriction to the von Neumann algebra is the identity.

theorem OAI.KadisonKastler.exists_contractive_weak_ultralimit line 22

Source documentation

Simultaneous weak limits preserve linearity and contractivity.

theorem exists_contractive_weak_ultralimit {ι : Type*} (ω : Ultrafilter ι)
    (F : ι → (H →L[ℂ] H) →L[ℂ] (H →L[ℂ] H)) (hF : ∀ i, ‖F i‖ ≤ 1) :
    ∃ E : (H →L[ℂ] H) →L[ℂ] (H →L[ℂ] H), ‖E‖ ≤ 1 ∧
      ∀ T x y, Tendsto (fun i => inner ℂ y (F i T x)) (ω : Filter ι)
        (𝓝 (inner ℂ y (E T x))) := by
…

theorem OAI.KadisonKastler.isInjective_of_trace_approximations line 54

Source documentation

A faithful vector identifies the limit map on the entire algebra.

theorem isInjective_of_trace_approximations {M : VonNeumannAlgebra H}
    (τ : TracialRepresentation M)
    (F : ℕ → (H →L[ℂ] H) →L[ℂ] (H →L[ℂ] H))
    (hF : ∀ n, ‖F n‖ ≤ 1) (hmem : ∀ n T, F n T ∈ M)
    (hfix : ∀ a : Algebra M, Tendsto (fun n => F n a.val τ.vector) atTop
      (𝓝 (a.val τ.vector))) : IsInjective M := by
…

Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.IsInjective