OAI/Analysis/DirectCrouzeix/HilbertSchmidt.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DirectCrouzeix.hsSq_eq_sum_norm_sq line 16
  2. def OAI.DirectCrouzeix.hsVector line 28
  3. theorem OAI.DirectCrouzeix.hsSq_eq_norm_hsVector_sq line 31
  4. theorem OAI.DirectCrouzeix.hsSq_conjTranspose line 35
  5. theorem OAI.DirectCrouzeix.hsSq_smul line 40
  6. def OAI.DirectCrouzeix.entryPair line 45
  7. theorem OAI.DirectCrouzeix.entryPair_conj line 48
  8. theorem OAI.DirectCrouzeix.hsSq_map_star line 58
  9. theorem OAI.DirectCrouzeix.hsSq_mul_le line 62
  10. theorem OAI.DirectCrouzeix.hsSq_mul_le_right line 85
  11. theorem OAI.DirectCrouzeix.entryPair_eq_inner line 92
  12. theorem OAI.DirectCrouzeix.norm_entryPair_sq_le line 97
  13. theorem OAI.DirectCrouzeix.norm_sum_entryPair_sq_le line 105