theorem adding_link_increases_gap
(net₁ net₂ : ComplementarityNetwork J)
(hw : ∀ j k, 0 ≤ net₁.w j k)
(hle : ∀ j k, net₁.w j k ≤ net₂.w j k) :
spectralGap net₁ ≤ spectralGap net₂ := by
-- Courant-Fischer minimax: λ₂ = min_{v⊥1} v^T L v / v^T v.
-- Increasing weights increases the numerator for all v.
simp only [spectralGap]
set S := {v : Fin J → ℝ | orthToOne J v ∧ vecNormSq J v > 0}
set R₁ := (fun v => laplacianQF net₁ v / vecNormSq J v) '' S
set R₂ := (fun v => laplacianQF net₂ v / vecNormSq J v) '' S
-- Case: S empty (J < 2) → both sInf ∅ = 0
by_cases hne : S.Nonempty
· -- BddBelow R₁: all Rayleigh quotients ≥ 0 (nonneg weights)
have hbdd : BddBelow R₁ := by
use 0; intro r ⟨u, ⟨_, hun⟩, hr⟩
rw [← hr]
exact div_nonneg (laplacianQF_nonneg net₁ hw u) (le_of_lt hun)
-- For each r ∈ R₂, sInf R₁ ≤ r
-- sInf R₁ ≤ sInf R₂: for each v ∈ S, R₁(v) ≤ R₂(v), so sInf R₁ ≤ R₂(v) for all v
apply le_csInf (Set.Nonempty.image _ hne)
intro r₂ ⟨v, hv, hr₂⟩
-- sInf R₁ ≤ R₁(v) ≤ R₂(v) = r₂
have hmem : laplacianQF net₁ v / vecNormSq J v ∈ R₁ := ⟨v, hv, rfl⟩
have hL_le : laplacianQF net₁ v ≤ laplacianQF net₂ v := by
unfold laplacianQF
apply mul_le_mul_of_nonneg_left _ (by norm_num : (0:ℝ) ≤ 1/2)
apply Finset.sum_le_sum; intro j _
apply Finset.sum_le_sum; intro k _
exact mul_le_mul_of_nonneg_right (hle j k) (sq_nonneg _)
calc sInf R₁ ≤ laplacianQF net₁ v / vecNormSq J v := csInf_le hbdd hmem
_ ≤ laplacianQF net₂ v / vecNormSq J v :=
div_le_div_of_nonneg_right hL_le (le_of_lt hv.2)
_ = r₂ := hr₂
· -- S empty: both images empty, sInf ∅ = sInf ∅
have hR₁_empty : R₁ = ∅ := Set.image_eq_empty.mpr (Set.not_nonempty_iff_eq_empty.mp hne)
have hR₂_empty : R₂ = ∅ := Set.image_eq_empty.mpr (Set.not_nonempty_iff_eq_empty.mp hne)
rw [hR₁_empty, hR₂_empty]CES on Networks: Heterogeneous Pairwise Complementarity