OAI/Analysis/KadisonKastler/PartitionProjectionGap.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

One projection retains a finite pinching gap

This is the finite sign-averaging argument in Haagerup, Acta Math. 158 (1987), Lemma 2.16. The reference error is bounded uniformly over all signs.

  1. def OAI.KadisonKastler.symmetryPositiveProjection line 28
  2. theorem OAI.KadisonKastler.symmetryPositiveProjection_defect line 38
  3. theorem OAI.KadisonKastler.partition_sign_defect_on_pinching line 47
  4. theorem OAI.KadisonKastler.exists_partition_projection_gap line 61