CountableRowCompletion.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Finite normalization preserves weak limits of countable row averages.

def OAI.KadisonKastler.initialRow line 25

theorem OAI.KadisonKastler.rowRemainder_tendsto_zero line 30

Source documentation

Weak convergence of the row mass to the identity makes the missing square root converge strongly to zero.

theorem rowRemainder_tendsto_zero {M : VonNeumannAlgebra H}
    (r : ℕ → Algebra M) (hr : ∀ n, rowSquare (initialRow r n) ≤ 1)
    (ht : ∀ ξ η, Tendsto
      (fun n => inner ℂ η (((rowSquare (initialRow r n) : Algebra M) : H →L[ℂ] H) ξ))
      atTop (𝓝 (inner ℂ η ξ))) (ξ : H) :
    Tendsto (fun n => ((rowRemainder (initialRow r n) : Algebra M) : H →L[ℂ] H) ξ) atTop (𝓝 0) := by
…

Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.rowSquare, OAI.KadisonKastler.initialRow, OAI.KadisonKastler.rowRemainder

theorem OAI.KadisonKastler.completedRow_average_tendsto_sub_zero line 50

theorem OAI.KadisonKastler.completedRow_average_weak_limit line 66

Source documentation

The normalized finite rows have every weak limit of the original partial rows. The map being averaged is allowed to be nonnormal.

theorem completedRow_average_weak_limit {M : VonNeumannAlgebra H}
    (r : ℕ → Algebra M) (hr : ∀ n, rowSquare (initialRow r n) ≤ 1)
    (ht : ∀ ξ η, Tendsto
      (fun n => inner ℂ η (((rowSquare (initialRow r n) : Algebra M) : H →L[ℂ] H) ξ))
      atTop (𝓝 (inner ℂ η ξ)))
    {F : Algebra M →ₗ[ℂ] Algebra M} {c : ℝ} (hF : CompletelyBoundedBy F c) (hc : 0 ≤ c)
    (x y : Algebra M)
    (hy : ∀ ξ η, Tendsto
      (fun n => inner ℂ η ((finiteRightAverage (initialRow r n) F x : H →L[ℂ] H) ξ))
      atTop (𝓝 (inner ℂ η ((y : H →L[ℂ] H) ξ)))) :
    ∀ ξ η, Tendsto
      (fun n => inner ℂ η ((finiteRightAverage (completedRow (initialRow r n)) F x :
…

Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.rowSquare, OAI.KadisonKastler.initialRow, OAI.KadisonKastler.CompletelyBoundedBy, OAI.KadisonKastler.finiteRightAverage, OAI.KadisonKastler.completedRow