OAI/Analysis/HyperbolicCones/NormThreshold.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The exact scalar threshold of a positive semidefinite matrix.

  1. theorem OAI.Paper256.posSemidef_scalar_sub_iff line 12
  2. theorem OAI.Paper256.posSemidef_norm_threshold line 22
  3. theorem OAI.Paper256.posSemidef_gram_threshold line 37