OAI/Analysis/BoundedHochschild/CountableMatrixBarOperators.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The degree-bounded weak-star limits of the finite matrix-section bar operators. These use the same groups and ultrafilter as the matrix cochain projection.

  1. def OAI.BoundedHochschild.KadisonRingrose.matrixSectionBarOperator line 20
  2. lemma OAI.BoundedHochschild.KadisonRingrose.matrixSectionBarOperator_norm line 25
  3. lemma OAI.BoundedHochschild.KadisonRingrose.matrixSectionBarOperator_add line 30
  4. lemma OAI.BoundedHochschild.KadisonRingrose.matrixSectionBarOperator_smul line 36
  5. lemma OAI.BoundedHochschild.KadisonRingrose.matrix_bar_limit_exists line 42
  6. def OAI.BoundedHochschild.KadisonRingrose.countableMatrixBarOperator line 51
  7. lemma OAI.BoundedHochschild.KadisonRingrose.countableMatrixBarOperator_norm line 56
  8. lemma OAI.BoundedHochschild.KadisonRingrose.countableMatrixBarOperator_tendsto line 62
  9. lemma OAI.BoundedHochschild.KadisonRingrose.countableMatrixBarOperator_add line 69
  10. lemma OAI.BoundedHochschild.KadisonRingrose.countableMatrixBarOperator_smul line 78
  11. def OAI.BoundedHochschild.KadisonRingrose.countableMatrixBarOperatorCLM line 87