OAI/Analysis/HyperbolicCones/CongruenceMaps.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Linear congruence maps and preservation of a two-block matrix pencil.

  1. def OAI.Paper256.congruenceSym line 12
  2. theorem OAI.Paper256.congruenceSym_val line 26
  3. def OAI.Paper256.congruenceRect line 29
  4. theorem OAI.Paper256.congruenceRect_apply line 35
  5. theorem OAI.Paper256.congruenceSym_positive line 38
  6. theorem OAI.Paper256.congruenceSym_inverseSquareRoot_self line 43
  7. theorem OAI.Paper256.block_congruence_identity line 48
  8. theorem OAI.Paper256.block_congruence_posSemidef_iff line 58