Same-eigenbasis simplifications for the explicit CFC.log resolvent remainder

This module only simplifies the explicit finite-cutoff remainder from LogResolvent.derivSAAtCutoffRemainder when the multiplier and probe direction are diagonal in the eigenbasis of the positive base point.

It does not remove the cutoff, prove a sign, or claim Epstein/Lieb/Tropp.

theorem HighDimProb.LogResolvent.derivSAAtCutoffRemainder_eq_sum_conjDiagonal {n : ℕ} (M B C : CFCLog.Carrier n) (T : ℝ) {b c : Fin n → ℝ} (hB : star ↑⋯.eigenvectorUnitary * ↑B * ↑⋯.eigenvectorUnitary = Matrix.diagonal b) (hC : star ↑⋯.eigenvectorUnitary * ↑C * ↑⋯.eigenvectorUnitary = Matrix.diagonal c) : derivSAAtCutoffRemainder M B C T = ∑ i : Fin n, b i * c i * ((matrixExpDividedDifferenceSeries (Real.log (⋯.eigenvalues i)) (Real.log (⋯.eigenvalues i)))⁻¹ - ∫ (s : ℝ) in 0..T, (⋯.eigenvalues i + s)⁻¹ * (⋯.eigenvalues i + s)⁻¹)

If the multiplier and probe direction are diagonal in the eigenbasis of the base point, the explicit cutoff remainder collapses to a single eigenvalue sum.

The cutoff integral remains explicit. This is a concrete same-eigenbasis specialization, not a cutoff-removal theorem.

theorem HighDimProb.LogResolvent.derivSAAtCutoffRemainder_eq_sum_inv_sub_kernel_conjDiagonal_of_strictlyPositive {n : ℕ} (M B C : CFCLog.Carrier n) (hPos : (selfAdjointStrictlyPositiveSet n).Mem M) (T : ℝ) {b c : Fin n → ℝ} (hB : star ↑⋯.eigenvectorUnitary * ↑B * ↑⋯.eigenvectorUnitary = Matrix.diagonal b) (hC : star ↑⋯.eigenvectorUnitary * ↑C * ↑⋯.eigenvectorUnitary = Matrix.diagonal c) : derivSAAtCutoffRemainder M B C T = ∑ i : Fin n, b i * c i * ((⋯.eigenvalues i)⁻¹ - ∫ (s : ℝ) in 0..T, (⋯.eigenvalues i + s)⁻¹ * (⋯.eigenvalues i + s)⁻¹)

Under strict positivity, the same-eigenbasis remainder simplifies further: the diagonal reciprocal divided-difference coefficient becomes the reciprocal eigenvalue of the positive base point.

The finite-cutoff kernel integral is still explicit.