Documentation

Lean 4 Proof

theorem uniform_laplacianQF_eq (ρ : ℝ) (v : Fin J → ℝ) :
    laplacianQF (uniformNetwork J ρ) v =
    (1 - ρ) * (↑J * ∑ j : Fin J, v j ^ 2 - (∑ j : Fin J, v j) ^ 2) := by
  -- The algebraic identity: for uniform weight w = (1-ρ),
  -- Strategy: rewrite if-then-else, factor out (1-ρ), use diagonal=0,
  -- then show Σ_{j,k} (v_j-v_k)² = 2(J·Σv² - (Σv)²).
  -- Strategy: reduce to the sum identity Σ_{j,k} (v_j-v_k)² = 2(J·Σv² - (Σv)²)
  simp only [laplacianQF, uniformNetwork]
  -- Rewrite: (if j=k then 0 else (1-ρ)) · (v_j-v_k)² = (1-ρ) · (v_j-v_k)²
  --   because diagonal terms have (v_j-v_j)²=0
  have entry_rw : ∀ j k : Fin J,
      (if j = k then (0 : ℝ) else (1 - ρ)) * (v j - v k) ^ 2 =
      (1 - ρ) * (v j - v k) ^ 2 := by
    intro j k; by_cases h : j = k
    · simp [h]
    · simp [h]
  simp_rw [entry_rw, ← Finset.mul_sum]
  -- Goal: (1/2) * ((1-ρ) * Σ_j Σ_k (v_j-v_k)²) = (1-ρ) * (J·Σv² - (Σv)²)
  -- Suffices to show: Σ_j Σ_k (v_j-v_k)² = 2 * (J·Σv² - (Σv)²)
  suffices h : ∑ j : Fin J, ∑ k : Fin J, (v j - v k) ^ 2 =
      2 * (↑J * ∑ j : Fin J, v j ^ 2 - (∑ j : Fin J, v j) ^ 2) by
    rw [h]; ring
  -- Expand (v_j-v_k)²  and manipulate sums
  -- Each term: (v j - v k)^2 = v j ^2 - 2*v j*v k + v k^2
  -- Σ_j Σ_k v_j^2 = J * Σ v^2  [inner sum constant in k]
  -- Σ_j Σ_k v_k^2 = J * Σ v^2  [outer sum constant in j]
  -- Σ_j Σ_k v_j * v_k = (Σ v)^2
  -- Total = 2J·Σv^2 - 2(Σv)^2
  have sum_sq : (∑ j : Fin J, v j) ^ 2 = ∑ j : Fin J, ∑ k : Fin J, v j * v k := by
    rw [sq, Fintype.sum_mul_sum]
  -- Expand (v j - v k)^2 and split the double sum
  have hsub : ∀ j k : Fin J, (v j - v k) ^ 2 =
      v j ^ 2 + v k ^ 2 - 2 * (v j * v k) := by
    intro j k; ring
  simp_rw [hsub, Finset.sum_sub_distrib, Finset.sum_add_distrib]
  -- Σ_j Σ_k v_j^2 = J * Σ v^2
  have h1 : ∑ j : Fin J, ∑ _k : Fin J, v j ^ 2 =
      ↑J * ∑ j : Fin J, v j ^ 2 := by
    simp [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul,
          Finset.mul_sum]
  -- Σ_j Σ_k v_k^2 = J * Σ v^2
  have h2 : ∑ _j : Fin J, ∑ k : Fin J, v k ^ 2 =
      ↑J * ∑ k : Fin J, v k ^ 2 := by
    simp [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
  -- Σ_j Σ_k 2*v_j*v_k = 2*(Σv)^2
  have h3 : ∑ j : Fin J, ∑ k : Fin J, (2 * (v j * v k)) =
      2 * (∑ j : Fin J, v j) ^ 2 := by
    rw [sq, Fintype.sum_mul_sum, Finset.mul_sum]
    congr 1; ext j; rw [Finset.mul_sum]
  rw [h1, h2, h3, sum_sq]; ring

Dependency Graph

Used by

Location

thesis/CESProofs/CurvatureRoles/NetworkCES.lean:155

Module Section

CES on Networks: Heterogeneous Pairwise Complementarity

In the same file