OAI/Analysis/KadisonKastler/TypeIIIInfinitesimal.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform infinitesimal estimate for all separably acting type III factors

The matrix corner is constructed from a proper isometry and the published comparison theorem. The tolerance therefore precedes the Hilbert space and factor without any matrix-corner hypothesis in the conclusion.

  1. theorem OAI.KadisonKastler.uniform_typeIII_selfAdjoint_estimate line 26