OAI/Analysis/KadisonKastler/InfinitesimalSequence.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Vanishing distance to the algebra plus its commutant

For a bounded sequence with asymptotically algebra-valued commutators, Sakai's theorem supplies the algebra part and the constructed matrix averaging supplies the commutant part. The full matrix corners here are actual data; their existence is not silently assumed as a published input.

  1. theorem OAI.KadisonKastler.typeIII_eventually_approximate_algebra_add_commutant line 32