OAI/Analysis/BoundedHochschild/MinimalRepresentedAverages.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Minimal families for represented right averages, and constancy of commutant-compressed norms. This is the first step of the minimal-family argument in Paulsen, J. Funct. Anal. 157 (1998), Theorem 5.8, pp. 378–379.

  1. def OAI.BoundedHochschild.KadisonRingrose.RepresentedRightAverageInvariant line 19
  2. theorem OAI.BoundedHochschild.KadisonRingrose.exists_minimal_represented_averages line 24