Trace-resolvent weighted trace monotonicity provider

This module adds the smallest honest weighted trace leaf needed around the resolvent perspective blocker: PSD numerators preserve Loewner monotonicity after applying trace on the right.

It does not prove mixed-numerator joint convexity, fixed-numerator shifted inverse convexity, relative-entropy joint convexity, Epstein, or Lieb.

theorem HighDimProb.trace_mul_mono_right_of_matrixLE_of_isPSDMatrix {n : ℕ} {T A B : Matrix (Fin n) (Fin n) ℝ} (hT : IsPSDMatrix T) (hAB : MatrixLE A B) : (T * A).trace ≤ (T * B).trace

PSD numerators preserve Loewner monotonicity after applying trace on the right.