Documentation

Lean 4 Proof

def interLevelQF (net : ComplementarityNetwork J) (P : HierarchicalPartition J N)
    (v : Fin J → ℝ) : ℝ :=
  (1 / 2) * ∑ j : Fin J, ∑ k : Fin J,
    (if P.level j ≠ P.level k then net.w j k else 0) * (v j - v k) ^ 2

Dependency Graph

Used by

Location

thesis/CESProofs/Hierarchy/EndogenousHierarchy.lean:66

Module Section

Endogenous Hierarchy: Network CES ↔ Spectral Hierarchy Bridge

In the same file