OAI/Analysis/BoundedHochschild/RowDefectCompletion.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A finite subrow of an infinite normalized row is completed by the square root of its positive defect. This completion does not assume a trace.

  1. def OAI.BoundedHochschild.KadisonRingrose.rowDefect line 17
  2. lemma OAI.BoundedHochschild.KadisonRingrose.rowDefect_nonneg line 20
  3. lemma OAI.BoundedHochschild.KadisonRingrose.rowDefect_mul_star line 23
  4. lemma OAI.BoundedHochschild.KadisonRingrose.rowDefect_norm_le line 29
  5. def OAI.BoundedHochschild.KadisonRingrose.completedRow line 37
  6. lemma OAI.BoundedHochschild.KadisonRingrose.completedRow_normalized line 41
  7. lemma OAI.BoundedHochschild.KadisonRingrose.completedRow_average line 54