OAI/Analysis/KadisonKastler/GoodProjectionCut.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Selecting one projection cut from averaged estimates

A small mean displacement and a strictly larger mean commutator gap give one cut satisfying both pointwise requirements. This is the scalar selection step in Haagerup's projection-cut argument.

  1. theorem OAI.KadisonKastler.exists_good_projection_cut_of_finite_measure line 22
  2. theorem OAI.KadisonKastler.exists_good_projection_cut line 50