Documentation

Lean 4 Proof

def isDisconnected (net : ComplementarityNetwork J) (P : HierarchicalPartition J N) : Prop :=
  ∀ j k : Fin J, P.level j ≠ P.level k → net.w j k = 0

Dependency Graph

Used by

Location

thesis/CESProofs/Hierarchy/EndogenousHierarchy.lean:146

Module Section

Endogenous Hierarchy: Network CES ↔ Spectral Hierarchy Bridge

In the same file