OAI/Analysis/JiangSu/TensorProducts/FaithfulTensorCrossNorm.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.NuclearUnitization.rectangle_bound line 12
  2. def OAI.NuclearUnitization.cut line 38
  3. lemma OAI.NuclearUnitization.cut_nonneg line 40
  4. lemma OAI.NuclearUnitization.cut_nonzero line 43
  5. lemma OAI.NuclearUnitization.cut_lower line 52
  6. lemma OAI.NuclearUnitization.commute_mul_le_mul_of_nonneg_right line 65
  7. lemma OAI.NuclearUnitization.faithful_pair_positive_norm line 70
  8. lemma OAI.NuclearUnitization.faithful_pair_norm line 125
  9. lemma OAI.NuclearUnitization.tmul_nonzero line 150
  10. def OAI.NuclearUnitization.leftMap line 161
  11. def OAI.NuclearUnitization.rightMap line 171
  12. lemma OAI.NuclearUnitization.cstar_norm_tmul line 181