Documentation

Lean 4 Proof

def spectralGap (net : ComplementarityNetwork J) : ℝ :=
  sInf ((fun v => laplacianQF net v / vecNormSq J v) ''
    {v : Fin J → ℝ | orthToOne J v ∧ vecNormSq J v > 0})

Dependency Graph

Used by

Location

thesis/CESProofs/CurvatureRoles/NetworkCES.lean:104

Module Section

CES on Networks: Heterogeneous Pairwise Complementarity

In the same file