OAI/Analysis/BoundedHochschild/PositiveProjectionGap.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A nonzero positive element dominates a positive multiple of a nonzero projection. This is the small spectral-cut consequence needed for the minimal averaging argument.

  1. theorem OAI.BoundedHochschild.KadisonRingrose.exists_positive_projection_gap line 19
  2. lemma OAI.BoundedHochschild.KadisonRingrose.projection_le_of_positive_gap line 46