OAI/Analysis/BoundedHochschild/FiniteFunctionAverages.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Deleting one independently averaged finite coordinate leaves the normalized average unchanged.

  1. lemma OAI.BoundedHochschild.KadisonRingrose.sum_removeNth line 15
  2. lemma OAI.BoundedHochschild.KadisonRingrose.normalized_sum_removeNth line 27