OAI/Analysis/BoundedHochschild/SubnormalizedOperatorRows.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Vector estimates for rows whose positive square sum is at most one. These estimates control tails when a normalized row has infinitely many entries.

  1. lemma OAI.BoundedHochschild.KadisonRingrose.sum_norm_adjoint_sq_le line 18
  2. lemma OAI.BoundedHochschild.KadisonRingrose.norm_sum_row_apply_sq_le line 38
  3. lemma OAI.BoundedHochschild.KadisonRingrose.operatorRowAverage_apply_sq_le line 58
  4. lemma OAI.BoundedHochschild.KadisonRingrose.operatorRowAverage_norm_le_of_le line 72