OAI/Analysis/KadisonKastler/SpatialStrong.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Bounded strong continuity of the spatial right representation

  1. theorem OAI.KadisonKastler.spatialRight_tendsto_strong line 20

    Source documentation

    A uniformly bounded strongly convergent family remains strongly convergent after amplification in the right tensor leg.

    theorem spatialRight_tendsto_strong
    {ι : Type*} {l : Filter ι} (T : ι → K →L[ℂ] K) (a : K →L[ℂ] K)
    {C : ℝ} (hT : ∀ i, ‖T i‖ ≤ C)
    (ha : ∀ y, Tendsto (fun i => T i y) l (𝓝 (a y)))
    (z : SpatialHilbert H K) :
    Tendsto (fun i => spatialRight (H := H) (T i) z) l
…

    Mentions: OAI.KadisonKastler.spatialRight