Problem 6: Large epsilon-light vertex subsets -- Loewner Pullback

Congruence pullbacks for Loewner order and epsilon-lightness from Loewner bound.

theorem Problem6.sqrt_pullback_loewner {V : Type u_1} [Fintype V] [DecidableEq V] (L Lhalf : Matrix V V ℝ) (hLhalf_herm : Lhalf.IsHermitian) (hLhalf_sq : Lhalf * Lhalf = L) (M : Matrix V V ℝ) (u : ℝ) (hM : (u • 1 - M).PosSemidef) : (u • L - Lhalf * M * Lhalf).PosSemidef

theorem Problem6.eps_light_of_loewner_bound {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (ε u : ℝ) (_hε : 0 < ε) (hu : u ≤ ε) (S : Finset V) (Lhalf : Matrix V V ℝ) (hLhalf_herm : Lhalf.IsHermitian) (hLhalf_sq : Lhalf * Lhalf = graphLaplacian G) (M : Matrix V V ℝ) (hM_bound : (u • 1 - M).PosSemidef) (hM_conn : Lhalf * M * Lhalf = inducedLaplacian G S) : IsEpsLight G ε S