Problem 6: Large epsilon-light vertex subsets -- One-Sided Barrier

One-sided barrier machinery for the BSS coloring argument.

theorem Problem6.barrier_smw_trace_bound {V : Type u_1} [Fintype V] [DecidableEq V] (M B : Matrix V V ℝ) (u u' : ℝ) (hu : u < u') (hM_bound : (u • 1 - M).PosDef) (hB : B.PosSemidef) (htrBU_lt : (B * (u' • 1 - M)⁻¹).trace < 1) (htrBU_nn : 0 ≤ (B * (u' • 1 - M)⁻¹).trace) (_htrBU2_nn : 0 ≤ (B * (u' • 1 - M)⁻¹ * (u' • 1 - M)⁻¹).trace) : barrierPotential u' (M + B) ≤ barrierPotential u' M + (B * (u' • 1 - M)⁻¹ * (u' • 1 - M)⁻¹).trace / (1 - (B * (u' • 1 - M)⁻¹).trace)

theorem Problem6.one_sided_barrier {V : Type u_1} [Fintype V] [DecidableEq V] (M B : Matrix V V ℝ) (u u' : ℝ) (hu : u < u') (hM_bound : (u • 1 - M).PosDef) (hB : B.PosSemidef) (hbarrier : have U := (u' • 1 - M)⁻¹; (B * U).trace + (B * U * U).trace / (barrierPotential u M - barrierPotential u' M) ≤ 1) : barrierPotential u' (M + B) ≤ barrierPotential u M

theorem Problem6.inv_sub_posDef_of_trace_lt_one {V : Type u_1} [Fintype V] [DecidableEq V] (U B : Matrix V V ℝ) (hU : U.PosDef) (hB : B.PosSemidef) (htr : (B * U).trace < 1) : (U⁻¹ - B).PosDef