Problem 6: Large epsilon-light vertex subsets -- Dynamic Coloring

Key infrastructure for the dynamic BSS coloring: pseudo-inverse pullback, projection identity, normalized monochromatic PSD.

theorem Problem6.inducedLaplacian_posSemidef {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) : (inducedLaplacian G S).PosSemidef

theorem Problem6.inducedLaplacian_le_graphLaplacian {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) : (graphLaplacian G - inducedLaplacian G S).PosSemidef

theorem Problem6.hermitian_mulVec_zero_of_sq_zero {V : Type u_1} [Fintype V] (Lhalf : Matrix V V ℝ) (hLhalf_herm : Lhalf.IsHermitian) (x : V → ℝ) (hx : (Lhalf * Lhalf).mulVec x = 0) : Lhalf.mulVec x = 0

theorem Problem6.pinv_pullback_eq {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) (Lhalf Lhalf_pinv : Matrix V V ℝ) (hLhalf_herm : Lhalf.IsHermitian) (hpinv_herm : Lhalf_pinv.IsHermitian) (hLhalf_sq : Lhalf * Lhalf = graphLaplacian G) (hMP1 : Lhalf * Lhalf_pinv * Lhalf = Lhalf) (hMP3 : Lhalf * Lhalf_pinv * (Lhalf * Lhalf_pinv) = Lhalf * Lhalf_pinv) (hMP4 : Lhalf * Lhalf_pinv = Lhalf_pinv * Lhalf) : Lhalf * (Lhalf_pinv * inducedLaplacian G S * Lhalf_pinv) * Lhalf = inducedLaplacian G S

theorem Problem6.normalized_mono_psd {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (Lhalf_pinv : Matrix V V ℝ) (hpinv_herm : Lhalf_pinv.IsHermitian) (S : Finset V) : (Lhalf_pinv * inducedLaplacian G S * Lhalf_pinv).PosSemidef

theorem Problem6.normalized_laplacian_eq_proj {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (Lhalf Lhalf_pinv : Matrix V V ℝ) (hLhalf_sq : Lhalf * Lhalf = graphLaplacian G) (hMP3 : Lhalf * Lhalf_pinv * (Lhalf * Lhalf_pinv) = Lhalf * Lhalf_pinv) (hMP4 : Lhalf * Lhalf_pinv = Lhalf_pinv * Lhalf) : Lhalf_pinv * graphLaplacian G * Lhalf_pinv = Lhalf * Lhalf_pinv

theorem Problem6.proj_le_one {V : Type u_1} [Fintype V] [DecidableEq V] (P : Matrix V V ℝ) (hP_herm : P.IsHermitian) (hP_idem : P * P = P) : (1 - P).PosSemidef

theorem Problem6.inducedLaplacian_mono {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (S T : Finset V) (hST : S ⊆ T) : (inducedLaplacian G T - inducedLaplacian G S).PosSemidef

theorem Problem6.psd_sub_sum_le {V : Type u_1} [DecidableEq V] {r : ℕ} (M : Fin r → Matrix V V ℝ) (u : ℝ) (hM_psd : ∀ (γ : Fin r), (M γ).PosSemidef) (h_total : (u • 1 - ∑ γ : Fin r, M γ).PosSemidef) (γ : Fin r) : (u • 1 - M γ).PosSemidef