Documentation

Lean 4 Proof

theorem hierarchy_is_spectral_decomposition
    (net : ComplementarityNetwork J) (P : HierarchicalPartition J N)
    (_hnd : ∃ ε, ε < 1 ∧ isNearDecomposable net P ε) :
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Hierarchy/EndogenousHierarchy.lean:489

Module Section

Endogenous Hierarchy: Network CES ↔ Spectral Hierarchy Bridge

In the same file