RowVectorEstimate.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Vector estimates for truncating the countable rows in module averaging.

def OAI.KadisonKastler.algebraRow line 26
theorem OAI.KadisonKastler.algebraRow_apply line 29
def OAI.KadisonKastler.rowAdjointVector line 32
theorem OAI.KadisonKastler.rowAdjointVector_norm_sq line 36
theorem OAI.KadisonKastler.finiteRightAverage_vector_bound line 59
Source documentation
The tail is controlled by the adjoint row on the chosen vector, even when the completely bounded map is not normal.
```
theorem finiteRightAverage_vector_bound {M : VonNeumannAlgebra H}
    {n : ℕ} (r : Fin n → Algebra M)
    {F : Algebra M →ₗ[ℂ] Algebra M} {c : ℝ}
    (hF : CompletelyBoundedBy F c) (hc : 0 ≤ c) (x : Algebra M) (ξ : H) :
    ‖(finiteRightAverage r F x : H →L[ℂ] H) ξ‖ ≤
      c * ‖x‖ * ‖algebraRow r‖ * ‖rowAdjointVector r ξ‖ := by
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.CompletelyBoundedBy, OAI.KadisonKastler.finiteRightAverage, OAI.KadisonKastler.algebraRow, OAI.KadisonKastler.rowAdjointVector