Documentation

Lean 4 Proof

def effectiveLevelRho (net : ComplementarityNetwork J)
    (P : HierarchicalPartition J N) (n : Fin N) : ℝ :=
  1 - effectiveLevelCurvature net P n

Dependency Graph

Used by

Location

thesis/CESProofs/Hierarchy/EndogenousHierarchy.lean:284

Module Section

Endogenous Hierarchy: Network CES ↔ Spectral Hierarchy Bridge

In the same file