OAI/Analysis/BoundedHochschild/MultimodularMatrixBound.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A bounded multimodular cochain has completely bounded last slices if the coefficient subalgebra contains unital isometry columns of every finite size. This is the required matrix-norm specialization, with no dimension factor in the bound.

  1. lemma OAI.BoundedHochschild.KadisonRingrose.columnDiagonal_eq_reconstruction line 20
  2. lemma OAI.BoundedHochschild.KadisonRingrose.columnReconstruction_norm_for_multimodular line 25
  3. lemma OAI.BoundedHochschild.KadisonRingrose.columnDiagonal_norm_le line 33
  4. lemma OAI.BoundedHochschild.KadisonRingrose.multimodular_matrix_identity line 41
  5. lemma OAI.BoundedHochschild.KadisonRingrose.multimodular_last_matrix_bound line 63
  6. theorem OAI.BoundedHochschild.KadisonRingrose.lastSliceEstimate_of_multimodular_columns line 80
  7. theorem OAI.BoundedHochschild.KadisonRingrose.primitive_of_multimodular_columns line 97