Documentation

Lean 4 Proof

theorem uniformNetwork_degree (ρ : ℝ) (j : Fin J) :
    vertexDegree (uniformNetwork J ρ) j = (↑J - 1) * (1 - ρ) := by
  simp only [vertexDegree, uniformNetwork]
  -- Σ_k (if j=k then 0 else (1-ρ))
  -- Rewrite: f(k) = (1-ρ) - (if j=k then (1-ρ) else 0)
  -- Σ f(k) = J·(1-ρ) - (1-ρ) = (J-1)·(1-ρ)
  have : ∀ k : Fin J, (if j = k then (0 : ℝ) else (1 - ρ)) =
      (1 - ρ) - (if j = k then (1 - ρ) else 0) := by
    intro k; split_ifs <;> ring
  simp_rw [this, Finset.sum_sub_distrib, Finset.sum_const, Finset.card_univ,
            Fintype.card_fin, nsmul_eq_mul, Finset.sum_ite_eq, Finset.mem_univ, ite_true]
  ring

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/NetworkCES.lean:307

Module Section

CES on Networks: Heterogeneous Pairwise Complementarity

In the same file