Documentation

Lean 4 Proof

def isNearDecomposable (net : ComplementarityNetwork J)
    (P : HierarchicalPartition J N) (ε : ℝ) : Prop :=
  ∀ j k : Fin J, P.level j ≠ P.level k → net.w j k ≤ ε

Dependency Graph

Used by

Location

thesis/CESProofs/Hierarchy/EndogenousHierarchy.lean:175

Module Section

Endogenous Hierarchy: Network CES ↔ Spectral Hierarchy Bridge

In the same file