Documentation

Lean 4 Proof

def levelSize (P : HierarchicalPartition J N) (n : Fin N) : ℕ :=
  (Finset.univ.filter fun j : Fin J => P.level j = n).card

Dependency Graph

Used by

Location

thesis/CESProofs/Hierarchy/EndogenousHierarchy.lean:237

Module Section

Endogenous Hierarchy: Network CES ↔ Spectral Hierarchy Bridge

In the same file