OAI/Analysis/KadisonKastler/UniformInfinitesimalBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The uniform linear infinitesimal estimate with matrix-corner data

Subtract a self-adjoint approximating sum and normalize by its distance. The bounded cutoff then contradicts any failure of the linear estimate. No closedness of the algebra-plus-commutant sum is used.

  1. theorem OAI.KadisonKastler.infinitesimal_bound_of_cutoff line 24
  2. theorem OAI.KadisonKastler.uniform_typeIII_infinitesimal_bound line 96