Documentation

Lean 4 Proof

def intraLevelQF (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:58

Module Section

Endogenous Hierarchy: Network CES ↔ Spectral Hierarchy Bridge

In the same file