OAI/Analysis/BoundedHochschild/InfiniteAveragingLimits.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Infinite normalized right averages are actual algebra-valued maps in the original finite-averaging orbit closure, with the original factorization bound.

  1. lemma OAI.BoundedHochschild.KadisonRingrose.normal_factorization_value_norm_le line 21
  2. lemma OAI.BoundedHochschild.KadisonRingrose.completed_averages_predual_tendsto line 31
  3. theorem OAI.BoundedHochschild.KadisonRingrose.exists_infinite_right_average line 61