WeakCPLimits.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Positivity and norm bounds in pointwise weak operator limits

These lemmas retain the complete positivity of the maps obtained from finite Hilbert-space tests. No normality of the limiting map is needed.

theorem OAI.KadisonKastler.isPositive_of_weak_limit line 26

Source documentation

Operator positivity is closed under convergence of every coefficient.

theorem isPositive_of_weak_limit (T : ι → H →L[ℂ] H) (S : H →L[ℂ] H)
    (hT : ∀ i, (T i).IsPositive)
    (ht : ∀ x y, Tendsto (fun i => inner ℂ y (T i x)) l (𝓝 (inner ℂ y (S x)))) :
    S.IsPositive := by
…

theorem OAI.KadisonKastler.norm_le_of_weak_limit line 53

Source documentation

A uniform operator norm bound survives a weak coefficient limit.

theorem norm_le_of_weak_limit {K : Type*} [NormedAddCommGroup K]
    [InnerProductSpace ℂ K] (T : ι → H →L[ℂ] K) (S : H →L[ℂ] K)
    {C : ℝ} (hC : 0 ≤ C) (hT : ∀ i, ‖T i‖ ≤ C)
    (ht : ∀ x y, Tendsto (fun i => inner ℂ y (T i x)) l (𝓝 (inner ℂ y (S x)))) :
    ‖S‖ ≤ C := by
…

theorem OAI.KadisonKastler.weak_limit_mem_of_weak_approximants line 75

Source documentation

Weak approximants from a fixed von Neumann algebra retain the limit in that algebra; uniform approximation in operator norm is unnecessary.

theorem weak_limit_mem_of_weak_approximants (N : VonNeumannAlgebra H)
    (T : ι → H →L[ℂ] H) (S : H →L[ℂ] H) (a : ι → Algebra N)
    (ht : ∀ x y, Tendsto (fun i => inner ℂ y (T i x)) l
      (𝓝 (inner ℂ y (S x))))
    (ha : ∀ x y, Tendsto (fun i => inner ℂ y (((a i : H →L[ℂ] H) - T i) x))
      l (𝓝 0)) : S ∈ N := by
…

Mentions: OAI.KadisonKastler.Algebra

theorem OAI.KadisonKastler.hilbertMatrix_weak_limit line 92

Source documentation

Entrywise weak convergence gives weak convergence of each finite operator-matrix amplification.

theorem hilbertMatrix_weak_limit (T : ι → CStarMatrix n n (H →L[ℂ] H))
    (S : CStarMatrix n n (H →L[ℂ] H))
    (ht : ∀ j k x y, Tendsto (fun i => inner ℂ y (T i j k x)) l
      (𝓝 (inner ℂ y (S j k x))))
    (x y : Generator.FiniteHilbert n H) :
    Tendsto (fun i => inner ℂ y (hilbertMatrix (T i) x)) l
      (𝓝 (inner ℂ y (hilbertMatrix S x))) := by
…

Mentions: OAI.Generator.FiniteHilbert, OAI.KadisonKastler.hilbertMatrix

theorem OAI.KadisonKastler.rectangularHilbertMatrix_weak_limit line 105

Source documentation

The same coefficient limit statement for rectangular amplifications.

theorem rectangularHilbertMatrix_weak_limit {m : Type*} [Fintype m]
    (T : ι → CStarMatrix m n (H →L[ℂ] H)) (S : CStarMatrix m n (H →L[ℂ] H))
    (ht : ∀ j k x y, Tendsto (fun i => inner ℂ y (T i j k x)) l
      (𝓝 (inner ℂ y (S j k x))))
    (x : Generator.FiniteHilbert n H) (y : Generator.FiniteHilbert m H) :
    Tendsto (fun i => inner ℂ y (rectangularHilbertMatrix (T i) x)) l
      (𝓝 (inner ℂ y (rectangularHilbertMatrix S x))) := by
…

Mentions: OAI.Generator.FiniteHilbert, OAI.KadisonKastler.rectangularHilbertMatrix

def OAI.KadisonKastler.completelyPositive_of_pointwise_weak_limit line 119

Source documentation

A pointwise weak limit, once bundled linearly, is completely positive.

def completelyPositive_of_pointwise_weak_limit
    (F : ι → A →CP (H →L[ℂ] H)) (S : A →ₗ[ℂ] (H →L[ℂ] H))
    (ht : ∀ a x y, Tendsto (fun i => inner ℂ y (F i a x)) l
      (𝓝 (inner ℂ y (S a x)))) : A →CP (H →L[ℂ] H) where
…

theorem OAI.KadisonKastler.complete_bound_of_pointwise_weak_limit line 146

Source documentation

A uniform complete bound survives a pointwise weak limit.

theorem complete_bound_of_pointwise_weak_limit
    (F : ι → A →ₗ[ℂ] (H →L[ℂ] H)) (S ρ : A →ₗ[ℂ] (H →L[ℂ] H))
    (ht : ∀ a x y, Tendsto (fun i => inner ℂ y (F i a x)) l
      (𝓝 (inner ℂ y (S a x))))
    {e : ℝ} (he : 0 ≤ e) (hF : ∀ i, CompletelyBoundedBy (F i - ρ) e) :
    CompletelyBoundedBy (S - ρ) e := by
…

Mentions: OAI.KadisonKastler.CompletelyBoundedBy

theorem OAI.KadisonKastler.exists_unitalCP_weak_ultralimit line 170

Source documentation

A family of unital completely positive maps has a simultaneous pointwise weak ultralimit. The limiting map is again unital and CP.

theorem exists_unitalCP_weak_ultralimit (ω : Ultrafilter ι)
    (F : ι → A →CP (H →L[ℂ] H)) (hF : ∀ i, F i 1 = 1) :
    ∃ S : A →CP (H →L[ℂ] H), S 1 = 1 ∧
      ∀ a x y, Tendsto (fun i => inner ℂ y (F i a x)) (ω : Filter ι)
        (𝓝 (inner ℂ y (S a x))) := by
…