Problem 6: Large epsilon-light vertex subsets -- Resolvent Bound

psd_resolvent_trace_bound: tr((U⁻¹ - B)⁻¹) ≤ tr(U) + tr(B·U²) / (1 - tr(B·U)).

theorem Problem6.psd_resolvent_trace_bound {V : Type u_1} [Fintype V] [DecidableEq V] (U B : Matrix V V ℝ) (hU : U.PosDef) (hB : B.PosSemidef) (htrBU_lt : (B * U).trace < 1) (_htrBU_nn : 0 ≤ (B * U).trace) : (U⁻¹ - B)⁻¹.trace ≤ U.trace + (B * U * U).trace / (1 - (B * U).trace)