OAI/Analysis/KadisonKastler/UniformPinchingGap.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A uniform test-vector gap for an admissible projection family

A maximal admissible family cannot have a small gap: its remaining corner would admit the strict refinement already constructed. This is the projection-family amplification of the local Haagerup witness.

  1. theorem OAI.KadisonKastler.maximal_admissibleFamily_gap line 23
  2. theorem OAI.KadisonKastler.exists_uniform_pinching_gap line 78