Documentation

Lean 4 Proof

def networkHessianQF (net : ComplementarityNetwork J) (c : ℝ) (v : Fin J → ℝ) : ℝ :=
  -(1 / ((↑J : ℝ) ^ 2 * c)) * laplacianQF net v

Dependency Graph

Used by

Location

thesis/CESProofs/CurvatureRoles/NetworkCES.lean:81

Module Section

CES on Networks: Heterogeneous Pairwise Complementarity

In the same file