OAI/Analysis/HyperbolicCones/InverseOrder.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Simultaneous spectral comparison of a positive matrix and its scalar shifts.

  1. theorem OAI.Paper256.matrix_cfc_affine line 12
  2. theorem OAI.Paper256.posDef_inverse_eq_cfc line 24
  3. theorem OAI.Paper256.posDef_shift_inverse_eq_cfc line 34
  4. theorem OAI.Paper256.posDef_inverse_sub_shift_inverse_posSemidef line 47