Documentation

Lean 4 Proof

def levelCoupling (net : ComplementarityNetwork J) (P : HierarchicalPartition J N)
    (n : Fin N) : ℝ :=
  ∑ j : Fin J, ∑ k : Fin J,
    if P.level j = n ∧ P.level k = n ∧ j ≠ k then net.w j k else 0

Dependency Graph

Used by

Location

thesis/CESProofs/Hierarchy/EndogenousHierarchy.lean:242

Module Section

Endogenous Hierarchy: Network CES ↔ Spectral Hierarchy Bridge

In the same file