OAI/Analysis/KadisonKastler/MultiplicationCorrectionSequence.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Iterating the quadratic cochain correction

A cochain with unit complete bound and quadratic coboundary remainder produces successive associative multiplications whose defects halve.

  1. structure OAI.KadisonKastler.SmallAssociativeProduct line 18
  2. def OAI.KadisonKastler.QuadraticCochainSolver line 25

    Source documentation

    The precise local cochain estimate used by the quadratic iteration.

    def QuadraticCochainSolver : Prop :=
…
  3. theorem OAI.KadisonKastler.exists_halving_multiplication_sequence line 33