theorem disconnected_zero_curvature (net : ComplementarityNetwork J)
(hw : ∀ j k, 0 ≤ net.w j k)
(hJ : 2 ≤ J)
(hdisconnected : spectralGap net = 0) :
∃ v : Fin J → ℝ, orthToOne J v ∧ (∃ j, v j ≠ 0) ∧
laplacianQF net v = 0 := by
-- Proof by contradiction using compactness of the unit sphere in 1⊥.
-- If no nontrivial null vector exists, L > 0 on the compact set
-- K = {v ⊥ 1 | Σvⱼ² = 1}, giving spectralGap ≥ min_K L > 0.
by_contra h_no_null
push_neg at h_no_null
-- h_no_null : ∀ v, orthToOne J v → (∃ j, v j ≠ 0) → laplacianQF net v ≠ 0
have hL_pos : ∀ v, orthToOne J v → vecNormSq J v > 0 → 0 < laplacianQF net v := by
intro v hv hvn
have hne : ∃ j, v j ≠ 0 := by
by_contra hall; push_neg at hall
exact absurd (Finset.sum_eq_zero (fun j _ => by simp [hall j]))
(ne_of_gt hvn : vecNormSq J v ≠ 0)
exact lt_of_le_of_ne (laplacianQF_nonneg net hw v) (Ne.symm (h_no_null v hv hne))
set K := {v : Fin J → ℝ | orthToOne J v ∧ vecNormSq J v = 1}
set i₀ : Fin J := ⟨0, by omega⟩
set i₁ : Fin J := ⟨1, by omega⟩
have h01 : i₀ ≠ i₁ := by simp [Fin.ext_iff]
-- K ⊆ closed unit ball (sup norm): |v_j| ≤ 1 since v_j² ≤ Σ v_k² = 1
have hK_sub : K ⊆ Metric.closedBall (0 : Fin J → ℝ) 1 := by
intro v ⟨_, hv_norm⟩
simp only [Metric.mem_closedBall, dist_pi_le_iff (by norm_num : (0:ℝ) ≤ 1)]
intro j
simp only [Pi.zero_apply, dist_zero_right, Real.norm_eq_abs]
have hvj_sq : v j ^ 2 ≤ 1 :=
calc v j ^ 2 ≤ ∑ k, v k ^ 2 :=
Finset.single_le_sum (fun k _ => sq_nonneg (v k)) (Finset.mem_univ j)
_ = 1 := hv_norm
have := sq_abs (v j); nlinarith
-- K is closed
have hK_closed : IsClosed K := by
apply IsClosed.inter
· exact isClosed_eq (continuous_finset_sum _ (fun _ _ => continuous_apply _))
continuous_const
· exact isClosed_eq (continuous_finset_sum _ (fun j _ =>
(continuous_apply j).pow 2)) continuous_const
-- K is compact (closed subset of compact ball in ProperSpace)
have hK_compact : IsCompact K :=
(isCompact_closedBall (0 : Fin J → ℝ) 1).of_isClosed_subset hK_closed hK_sub
-- L is continuous (finite sums of continuous functions)
have hL_cont : Continuous (laplacianQF net) := by
unfold laplacianQF
apply continuous_const.mul
apply continuous_finset_sum; intro j _
apply continuous_finset_sum; intro k _
exact continuous_const.mul (((continuous_apply j).sub (continuous_apply k)).pow 2)
-- K is nonempty: (1/√2)(e₀ - e₁) ∈ K
have hK_ne : K.Nonempty := by
set c := Real.sqrt 2
have hc_pos : 0 < c := Real.sqrt_pos_of_pos (by norm_num : (0:ℝ) < 2)
have hc_ne : c ≠ 0 := ne_of_gt hc_pos
have hc_sq : c ^ 2 = 2 := Real.sq_sqrt (by norm_num : (0:ℝ) ≤ 2)
set e : Fin J → ℝ := fun j => if j = i₀ then 1 else if j = i₁ then -1 else 0
have h10 : i₁ ≠ i₀ := Ne.symm h01
-- Sum of e = 0
have he_sum : ∑ j : Fin J, e j = 0 := by
simp only [e]
have : ∀ j : Fin J, (if j = i₀ then (1:ℝ) else if j = i₁ then -1 else 0) =
(if j = i₀ then (1:ℝ) else 0) + (if j = i₁ then (-1:ℝ) else 0) := by
intro j; by_cases h1 : j = i₀
· subst h1; simp [h01]
· by_cases h2 : j = i₁ <;> simp [h1, h2, h10]
simp_rw [this, Finset.sum_add_distrib, Finset.sum_ite_eq', Finset.mem_univ, ite_true]
norm_num
-- Sum of e² = 2
have he_sq : ∑ j : Fin J, e j ^ 2 = 2 := by
simp only [e]
have : ∀ j : Fin J, (if j = i₀ then (1:ℝ) else if j = i₁ then -1 else 0) ^ 2 =
(if j = i₀ then (1:ℝ) else 0) + (if j = i₁ then (1:ℝ) else 0) := by
intro j; by_cases h1 : j = i₀
· subst h1; simp [h01]
· by_cases h2 : j = i₁ <;> simp [h1, h2, h10]
simp_rw [this, Finset.sum_add_distrib, Finset.sum_ite_eq', Finset.mem_univ, ite_true]
norm_num
refine ⟨fun j => e j / c, ?_, ?_⟩
· -- orthToOne
change vecSum J (fun j => e j / c) = 0
simp only [vecSum]; rw [(Finset.sum_div _ _ _).symm, he_sum, zero_div]
· -- vecNormSq = 1
change ∑ j : Fin J, (e j / c) ^ 2 = 1
simp_rw [div_pow]; rw [(Finset.sum_div _ _ _).symm, he_sq, hc_sq]; norm_num
-- By compactness, L attains its minimum on K
obtain ⟨v_min, ⟨hv_orth, hv_norm⟩, hv_le⟩ :=
hK_compact.exists_isMinOn hK_ne hL_cont.continuousOn
-- L(v_min) > 0
have hv_pos : 0 < vecNormSq J v_min := by rw [hv_norm]; norm_num
have hL_min_pos : 0 < laplacianQF net v_min := hL_pos v_min hv_orth hv_pos
-- spectralGap ≥ L(v_min) > 0, contradicting hdisconnected = 0
-- For every v ∈ S, scale u = v/√s to get u ∈ K, L(u) = L(v)/s, and L(u) ≥ L(v_min)
have hge : laplacianQF net v_min ≤ spectralGap net := by
apply le_csInf
· exact ⟨_, ⟨v_min, ⟨hv_orth, hv_pos⟩, rfl⟩⟩
intro r ⟨v, ⟨hv_o, hvn⟩, hr⟩
rw [← hr]
set s := vecNormSq J v
set t := Real.sqrt s
have ht_pos : 0 < t := Real.sqrt_pos_of_pos hvn
have ht_ne : t ≠ 0 := ne_of_gt ht_pos
set u : Fin J → ℝ := fun j => v j / t
have hu_orth : orthToOne J u := by
simp only [orthToOne, vecSum, u]
rw [(Finset.sum_div _ _ t).symm]
simp only [orthToOne, vecSum] at hv_o
rw [hv_o, zero_div]
have hu_norm : vecNormSq J u = 1 := by
change ∑ j, (v j / t) ^ 2 = 1
simp_rw [div_pow]
rw [(Finset.sum_div _ _ _).symm, Real.sq_sqrt (le_of_lt hvn)]
exact div_self (ne_of_gt hvn)
have hL_u : laplacianQF net u = laplacianQF net v / s := by
simp only [laplacianQF, u]
have hsub : ∀ j k : Fin J, (v j / t - v k / t) ^ 2 = (v j - v k) ^ 2 / t ^ 2 := by
intro j k; rw [← sub_div, div_pow]
simp_rw [hsub, mul_div_assoc]
-- Each inner sum: Σ_k w*d²/t² = (Σ_k w*d²)/t²
have inner_rw : ∀ j : Fin J,
∑ k, net.w j k * (v j - v k) ^ 2 / t ^ 2 =
(∑ k, net.w j k * (v j - v k) ^ 2) / t ^ 2 := by
intro j; exact (Finset.sum_div _ _ _).symm
simp_rw [mul_div_assoc'] at inner_rw ⊢
simp_rw [inner_rw]
-- Outer sum: Σ_j (inner/t²) = (Σ_j inner)/t²
rw [(Finset.sum_div _ _ _).symm, mul_div_assoc,
Real.sq_sqrt (le_of_lt hvn)]
calc laplacianQF net v_min ≤ laplacianQF net u := hv_le ⟨hu_orth, hu_norm⟩
_ = laplacianQF net v / s := hL_u
_ = laplacianQF net v / vecNormSq J v := rfl
linarithCES on Networks: Heterogeneous Pairwise Complementarity