OAI/Analysis/BoundedHochschild/OperatorRowAverages.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The operator in a factorization remains bounded under normalized row averaging. Both represented rows are allowed to act on different Hilbert spaces.

  1. lemma OAI.BoundedHochschild.KadisonRingrose.sum_norm_adjoint_sq line 18
  2. lemma OAI.BoundedHochschild.KadisonRingrose.norm_sum_inner_sq_le line 40
  3. def OAI.BoundedHochschild.KadisonRingrose.operatorRowAverage line 48
  4. lemma OAI.BoundedHochschild.KadisonRingrose.operatorRowAverage_apply line 53
  5. theorem OAI.BoundedHochschild.KadisonRingrose.operatorRowAverage_norm_le line 58