OAI/Analysis/BoundedHochschild/CompactAverages.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Compact unitary averaging of Hochschild cochains.

  1. lemma OAI.BoundedHochschild.continuous_translateLast line 21
  2. lemma OAI.BoundedHochschild.integrable_translateLast line 50
  3. def OAI.BoundedHochschild.compactAverage line 55
  4. lemma OAI.BoundedHochschild.norm_compactAverage_le line 60
  5. lemma OAI.BoundedHochschild.compactAverage_fixed line 67
  6. lemma OAI.BoundedHochschild.compactAverage_residual line 77