Documentation

Lean 4 Proof

def uniformNetwork (J : ℕ) (ρ : ℝ) : ComplementarityNetwork J where
  w := fun j k => if j = k then 0 else (1 - ρ)
  symmetric := fun j k => by
    by_cases h : j = k
    · simp [h]
    · simp [h, Ne.symm h]
  zero_diag := fun j => by simp

Dependency Graph

Used by

Location

thesis/CESProofs/CurvatureRoles/NetworkCES.lean:59

Module Section

CES on Networks: Heterogeneous Pairwise Complementarity

In the same file