OAI/Analysis/TracialCohomology/Partitions.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Partitions for bounded Hochschild cohomology.

  1. lemma OAI.PopaMatrices.system_of_partition line 29
  2. lemma OAI.PopaMatrices.orthogonal_of_complement line 63
  3. lemma OAI.PopaMatrices.system_containing_rational_projection line 73
  4. lemma OAI.PopaCenter.system_of_central_partition line 132
  5. lemma OAI.PopaCenter.orthogonal_of_subprojections line 166
  6. lemma OAI.PopaCenter.halving_average line 175
  7. lemma OAI.PopaCenter.double_partition line 190
  8. lemma OAI.PopaCenter.dyadic_partition line 232
  9. theorem OAI.PopaCenter.exists_dyadic_system line 248
  10. lemma OAI.PopaCenter.central_smul_real line 263
  11. lemma OAI.PopaCenter.central_posPart line 269
  12. theorem OAI.PopaCenter.exists_central_dyadic_projection line 276
  13. theorem OAI.PopaCenter.central_dyadic_digits line 334