OAI/Analysis/KadisonKastler/UniformInfinitesimalCutoff.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A uniform infinitesimal cutoff for represented type III factors

The tolerance is chosen before the Hilbert space and factor. The estimate uses a countable full matrix corner.

  1. structure OAI.KadisonKastler.MatrixTypeIIIFactorModel line 20
  2. theorem OAI.KadisonKastler.uniform_typeIII_infinitesimal_cutoff line 42