Documentation

Lean 4 Proof

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

Dependency Graph

Used by

Location

thesis/CESProofs/Hierarchy/EndogenousHierarchy.lean:292

Module Section

Endogenous Hierarchy: Network CES ↔ Spectral Hierarchy Bridge

In the same file