OAI/Analysis/NumericalRange/HilbertSchmidt.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CompleteCrouzeix.hsSq line 35
  2. theorem OAI.CompleteCrouzeix.trace_mul_nonneg line 37
  3. theorem OAI.CompleteCrouzeix.trace_blocks line 45
  4. theorem OAI.CompleteCrouzeix.block_density_hs line 50
  5. abbrev OAI.CompleteCrouzeix.HSMatrix line 79
  6. def OAI.CompleteCrouzeix.toHS line 81
  7. def OAI.CompleteCrouzeix.fromHS line 82
  8. theorem OAI.CompleteCrouzeix.fromHS_toHS line 84
  9. theorem OAI.CompleteCrouzeix.toHS_fromHS line 86
  10. lemma OAI.CompleteCrouzeix.hsSq_eq_sum line 89
  11. lemma OAI.CompleteCrouzeix.norm_toHS_sq line 103
  12. lemma OAI.CompleteCrouzeix.block_density_norm line 107
  13. def OAI.CompleteCrouzeix.hsStar line 112
  14. lemma OAI.CompleteCrouzeix.hsStar_apply line 126
  15. lemma OAI.CompleteCrouzeix.hsStar_involutive line 128
  16. lemma OAI.CompleteCrouzeix.hs_left_contraction line 131
  17. lemma OAI.CompleteCrouzeix.hs_right_contraction line 150
  18. lemma OAI.CompleteCrouzeix.l2_norm_sq line 161
  19. lemma OAI.CompleteCrouzeix.l2_integrable_norm_sq line 168
  20. def OAI.CompleteCrouzeix.l2StarL line 174
  21. lemma OAI.CompleteCrouzeix.l2StarL_ae line 177
  22. lemma OAI.CompleteCrouzeix.l2StarL_involutive line 181
  23. lemma OAI.CompleteCrouzeix.l2StarL_norm line 187
  24. def OAI.CompleteCrouzeix.l2Star line 194
  25. lemma OAI.CompleteCrouzeix.l2Star_apply line 203
  26. lemma OAI.CompleteCrouzeix.hermitian_l2Star line 205
  27. theorem OAI.CompleteCrouzeix.block_density_l2 line 212
  28. def OAI.CompleteCrouzeix.hsLeft line 231
  29. def OAI.CompleteCrouzeix.hsRight line 241
  30. lemma OAI.CompleteCrouzeix.hsLeft_apply line 251
  31. lemma OAI.CompleteCrouzeix.hsRight_apply line 254
  32. lemma OAI.CompleteCrouzeix.hsLeft_norm line 258
  33. lemma OAI.CompleteCrouzeix.hsRight_norm line 262
  34. lemma OAI.CompleteCrouzeix.hs_inner line 267
  35. lemma OAI.CompleteCrouzeix.hsLeft_adjoint line 280
  36. lemma OAI.CompleteCrouzeix.hsRight_adjoint line 291
  37. def OAI.CompleteCrouzeix.hsLeftL line 303
  38. def OAI.CompleteCrouzeix.hsRightL line 313
  39. lemma OAI.CompleteCrouzeix.pointwise_memLp line 332
  40. def OAI.CompleteCrouzeix.pointwiseL2 line 339
  41. lemma OAI.CompleteCrouzeix.pointwiseL2_ae line 342
  42. lemma OAI.CompleteCrouzeix.pointwiseL2_norm line 346
  43. def OAI.CompleteCrouzeix.pointwiseL2L line 352
  44. lemma OAI.CompleteCrouzeix.pointwiseL2L_norm line 375
  45. lemma OAI.CompleteCrouzeix.pointwiseL2L_adjoint line 380