OAI/Analysis/BoundedHochschild/NormalInfiniteAverages.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Infinite normalized right averages remain valued in the original algebra. The proof realizes their lifted strong limits through the closed represented algebra balls, without a normality assumption on the auxiliary representation.

  1. lemma OAI.BoundedHochschild.KadisonRingrose.normalGNS_row_limit line 23
  2. theorem OAI.BoundedHochschild.KadisonRingrose.normal_infinite_average_realize line 31