OAI/Analysis/Steinitz/Spectral.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

Real spectral calculus and noncommuting matrix inequalities.

  1. lemma OAI.EuclideanSteinitz.Spectral.unitary_transpose_mul line 13
  2. lemma OAI.EuclideanSteinitz.Spectral.unitary_mul_transpose line 18
  3. lemma OAI.EuclideanSteinitz.Spectral.real_spectral line 23
  4. lemma OAI.EuclideanSteinitz.Spectral.real_cfc line 30
  5. lemma OAI.EuclideanSteinitz.Spectral.trace_cfc line 38
  6. lemma OAI.EuclideanSteinitz.Spectral.trace_spectral line 42
  7. lemma OAI.EuclideanSteinitz.Spectral.trace_conjugate line 47
  8. lemma OAI.EuclideanSteinitz.Spectral.trace_transpose_conjugate line 51
  9. lemma OAI.EuclideanSteinitz.Spectral.sum_row_squares line 55
  10. lemma OAI.EuclideanSteinitz.Spectral.sum_col_squares line 60
  11. lemma OAI.EuclideanSteinitz.Spectral.orthostochastic_sums line 65
  12. def OAI.EuclideanSteinitz.Spectral.overlapBasis line 69
  13. lemma OAI.EuclideanSteinitz.Spectral.overlapBasis_coe line 73
  14. lemma OAI.EuclideanSteinitz.Spectral.cfc_mixed_basis line 80
  15. lemma OAI.EuclideanSteinitz.Spectral.cfc_mixed_basis_apply line 90
  16. lemma OAI.EuclideanSteinitz.Spectral.trace_sandwich_diagonal line 99
  17. lemma OAI.EuclideanSteinitz.Spectral.trace_weighted_basis line 110
  18. lemma OAI.EuclideanSteinitz.Spectral.weighted_cfc_distance line 123
  19. lemma OAI.EuclideanSteinitz.Spectral.trace_diagonal_product line 136
  20. lemma OAI.EuclideanSteinitz.Spectral.trace_cfc_product line 148
  21. lemma OAI.EuclideanSteinitz.Spectral.overlap_sum_left line 170
  22. lemma OAI.EuclideanSteinitz.Spectral.overlap_sum_right line 174
  23. lemma OAI.EuclideanSteinitz.Spectral.trace_cfc_remainder line 179
  24. lemma OAI.EuclideanSteinitz.Spectral.convex_tangent line 216
  25. lemma OAI.EuclideanSteinitz.Spectral.trace_tangent_le line 227
  26. lemma OAI.EuclideanSteinitz.Spectral.hasDerivWithinAt_of_tangents line 242
  27. lemma OAI.EuclideanSteinitz.Spectral.trace_cfc_affine_derivative line 268
  28. lemma OAI.EuclideanSteinitz.Spectral.continuous_cfc_affine line 296
  29. lemma OAI.EuclideanSteinitz.Spectral.trace_rpow_affine_derivative line 305
  30. lemma OAI.EuclideanSteinitz.Spectral.trace_psd_pairing line 323
  31. lemma OAI.EuclideanSteinitz.Spectral.trace_convex_monotone line 332
  32. lemma OAI.EuclideanSteinitz.Spectral.trace_rpow_monotone line 350
  33. lemma OAI.EuclideanSteinitz.Spectral.trace_cfc_eq_of_charpoly line 362
  34. lemma OAI.EuclideanSteinitz.Spectral.transpose_contraction line 367
  35. lemma OAI.EuclideanSteinitz.Spectral.trace_rpow_contraction line 380