theorem uniform_spectralGap (hJ : 2 ≤ J) (ρ : ℝ) :
spectralGap (uniformNetwork J ρ) = ↑J * (1 - ρ) := by
simp only [spectralGap]
-- Every v ⊥ 1 with ‖v‖² > 0 gives Rayleigh quotient = J*(1-ρ)
-- by uniform_laplacianQF_on_perp. So the image is {J*(1-ρ)}.
-- Witness for nonemptiness: e₀ - e₁.
set i₀ : Fin J := ⟨0, by omega⟩
set i₁ : Fin J := ⟨1, by omega⟩
have h01 : i₀ ≠ i₁ := by simp [Fin.ext_iff, i₀, i₁]
-- Helper: for v ⊥ 1, the Rayleigh quotient on the uniform network is constant
have hquot : ∀ v : Fin J → ℝ, orthToOne J v → vecNormSq J v > 0 →
laplacianQF (uniformNetwork J ρ) v / vecNormSq J v = ↑J * (1 - ρ) := by
intro v hv hvn
rw [uniform_laplacianQF_on_perp ρ v hv]
field_simp
-- Construct witness w = e₀ - e₁
set w : Fin J → ℝ := fun j => if j = i₀ then 1 else if j = i₁ then -1 else 0
have hw_orth : orthToOne J w := by
simp only [orthToOne, vecSum, w]
have hrw : ∀ 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₁
· subst h2; simp [h1]
· simp [h1, h2]
simp_rw [hrw, Finset.sum_add_distrib, Finset.sum_ite_eq', Finset.mem_univ, ite_true]
norm_num
have hw_norm : vecNormSq J w > 0 := by
simp only [vecNormSq, w]
apply Finset.sum_pos'
· intro j _; exact sq_nonneg _
· exact ⟨i₀, Finset.mem_univ _, by simp⟩
-- Show the image is the singleton {J*(1-ρ)}
have himg : (fun v => laplacianQF (uniformNetwork J ρ) v / vecNormSq J v) ''
{v : Fin J → ℝ | orthToOne J v ∧ vecNormSq J v > 0} = {↑J * (1 - ρ)} := by
ext r; simp only [Set.mem_image, Set.mem_setOf_eq, Set.mem_singleton_iff]
constructor
· rintro ⟨v, ⟨hv, hvn⟩, hr⟩; rw [← hr]; exact hquot v hv hvn
· intro hr; exact ⟨w, ⟨hw_orth, hw_norm⟩, hr ▸ hquot w hw_orth hw_norm⟩
rw [himg, csInf_singleton]CES on Networks: Heterogeneous Pairwise Complementarity