OAI/Analysis/BoundedHochschild/InfiniteOperatorRows.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Strongly convergent operator rows. The left row need not be normal: the summability estimate uses the square-sum bound on the right row only.

  1. lemma OAI.BoundedHochschild.KadisonRingrose.summable_row_vectors line 21
  2. lemma OAI.BoundedHochschild.KadisonRingrose.summable_adjoint_row_sq line 40
  3. lemma OAI.BoundedHochschild.KadisonRingrose.summable_operator_row_apply line 49
  4. lemma OAI.BoundedHochschild.KadisonRingrose.tsum_operator_row_apply_norm_le line 60
  5. def OAI.BoundedHochschild.KadisonRingrose.infiniteOperatorRow line 78
  6. lemma OAI.BoundedHochschild.KadisonRingrose.infiniteOperatorRow_norm_le line 95
  7. lemma OAI.BoundedHochschild.KadisonRingrose.infiniteOperatorRow_hasSum line 103