OAI/Analysis/BoundedHochschild/InfiniteInvariantFamilies.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Closed families invariant under finite normalized averages are also invariant under every normalized infinite row for which an operator factorization is given. This justifies the infinite rows in the minimal-family argument without strengthening its invariance hypothesis.

  1. theorem OAI.BoundedHochschild.KadisonRingrose.infinite_average_mem_invariant_family line 23