OAI/Analysis/BoundedHochschild/InfiniteRepresentedAverages.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Infinite right averages are strong limits of finite normalized averages, and hence lie in the same weakly closed orbit. Only the target representation is required to preserve the normalization limit.

  1. lemma OAI.BoundedHochschild.KadisonRingrose.representation_row_le line 22
  2. def OAI.BoundedHochschild.KadisonRingrose.infiniteRepresentedRightAverage line 27
  3. lemma OAI.BoundedHochschild.KadisonRingrose.infiniteRepresentedRightAverage_norm_le line 34
  4. lemma OAI.BoundedHochschild.KadisonRingrose.infiniteRepresentedRightAverage_hasSum line 40
  5. lemma OAI.BoundedHochschild.KadisonRingrose.completedRow_average_tendsto line 48
  6. lemma OAI.BoundedHochschild.KadisonRingrose.infiniteRepresentedRightAverage_mem_closed_orbit line 66