OAI/Analysis/WeakInfiniteness/MatrixCutToolkit.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WeakPureInfiniteness.diagonalHom line 33
  2. lemma OAI.WeakPureInfiniteness.diagonalCopies_nonneg line 56
  3. lemma OAI.WeakPureInfiniteness.diagonalCopies_cfc line 65
  4. lemma OAI.WeakPureInfiniteness.left_identity_on_hereditary line 71
  5. lemma OAI.WeakPureInfiniteness.rectangular_sub_mul line 80
  6. lemma OAI.WeakPureInfiniteness.rectangular_mul_sub line 85
  7. lemma OAI.WeakPureInfiniteness.rectangular_star_sub line 90
  8. lemma OAI.WeakPureInfiniteness.rectangular_left_identity_of_range line 93
  9. lemma OAI.WeakPureInfiniteness.rectangular_left_identity_of_hereditary_range line 111
  10. def OAI.WeakPureInfiniteness.positiveCut line 116
  11. lemma OAI.WeakPureInfiniteness.positiveCut_nonneg line 118
  12. lemma OAI.WeakPureInfiniteness.spectralRamp_mul_positiveCut line 122