OAI/Analysis/HyperbolicCones/NormLimits.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The positive affine paths used in the norm identity and their matrix limits.

  1. theorem OAI.Paper256.matrix_mul_tendsto line 14
  2. theorem OAI.Paper256.affine_posDef line 22
  3. theorem OAI.Paper256.positive_unital_map_affine_posDef line 28
  4. theorem OAI.Paper256.positive_unital_map_inverseSquareRoot_tendsto line 35