OAI/Analysis/KadisonKastler/PositiveConeQuadraticSupport.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The left support of a modular quadratic vector

For a positive vector, the kernel of a J a J on that vector is already the kernel of the left action of a. This is the support calculation needed for faithful finite matrix averaging.

  1. theorem OAI.KadisonKastler.positiveCone_operator_kills_of_quadratic_kills line 23