Documentation

Lean 4 Proof

def meanComplementarity (net : ComplementarityNetwork J) : ℝ :=
  1 - (∑ j : Fin J, ∑ k : Fin J, net.w j k) / (↑J * (↑J - 1))

Dependency Graph

Used by

Location

thesis/CESProofs/CurvatureRoles/NetworkCES.lean:89

Module Section

CES on Networks: Heterogeneous Pairwise Complementarity

In the same file