OAI/Analysis/WeakInfiniteness/NuclearCP.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WeakPureInfiniteness.matrixLinearMap line 40
  2. lemma OAI.WeakPureInfiniteness.matrixLinearMap_apply line 48
  3. lemma OAI.WeakPureInfiniteness.matrixLinearMap_nonneg line 51
  4. lemma OAI.WeakPureInfiniteness.matrixLinearMap_mono line 55
  5. def OAI.WeakPureInfiniteness.matrixDiagonalHom line 63
  6. lemma OAI.WeakPureInfiniteness.matrixLinearMap_diagonal line 78
  7. lemma OAI.WeakPureInfiniteness.matrix_mul_diagonal_tendsto line 85
  8. lemma OAI.WeakPureInfiniteness.norm_matrixLinearMap_nonneg_le line 100
  9. lemma OAI.WeakPureInfiniteness.norm_matrixLinearMap_le line 144