Documentation

Lean 4 Proof

theorem uniformNetwork_meanComplementarity (hJ : 2 ≤ J) (ρ : ℝ) :
    meanComplementarity (uniformNetwork J ρ) = ρ := by
  simp only [meanComplementarity, uniformNetwork]
  -- Σ_j Σ_k (if j=k then 0 else (1-ρ)) = J(J-1)·(1-ρ)
  -- So 1 - J(J-1)(1-ρ) / (J(J-1)) = 1 - (1-ρ) = ρ
  have hJpos : (0 : ℝ) < ↑J := by exact_mod_cast (show 0 < J by omega)
  have hJ1pos : (0 : ℝ) < ↑J - 1 := by
    have : (1 : ℝ) < ↑J := by exact_mod_cast (show 1 < J by omega)
    linarith
  have hJJ1_ne : (↑J : ℝ) * (↑J - 1) ≠ 0 := ne_of_gt (mul_pos hJpos hJ1pos)
  -- Rewrite each entry: (if j=k then 0 else (1-ρ)) = (1-ρ) - (if j=k then (1-ρ) else 0)
  have entry_rw : ∀ j k : Fin J, (if j = k then (0 : ℝ) else (1 - ρ)) =
      (1 - ρ) - (if j = k then (1 - ρ) else 0) := by
    intro j k; split_ifs <;> ring
  simp_rw [entry_rw, 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]
  -- Now outer sum: Σ_j (J·(1-ρ) - (1-ρ)) = J·((J-1)·(1-ρ))
  simp only [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
  field_simp
  ring

Dependency Graph

Location

thesis/CESProofs/CurvatureRoles/NetworkCES.lean:268

Module Section

CES on Networks: Heterogeneous Pairwise Complementarity

In the same file