OAI/Analysis/KadisonKastler/MultiplicationCorrectionFromCochains.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

From the quadratic cochain estimate to multiplication correction

The analytic cochain selector is kept as an explicit argument. The product iteration and its complete bound are proved here, not postulated.

  1. theorem OAI.KadisonKastler.multiplication_correction_of_quadratic_cochains line 20