Documentation

Lean 4 Proof

def effectiveLevelCurvature (net : ComplementarityNetwork J)
    (P : HierarchicalPartition J N) (n : Fin N) : ℝ :=
  let J_n := levelSize P n
  if J_n ≤ 1 then 0
  else levelCoupling net P n / (↑J_n * (↑J_n - 1))

Dependency Graph

Used by

Location

thesis/CESProofs/Hierarchy/EndogenousHierarchy.lean:251

Module Section

Endogenous Hierarchy: Network CES ↔ Spectral Hierarchy Bridge

In the same file