Documentation

Lean 4 Proof

theorem eigenvalue_clustering_partition
    {M : ℕ} (_spec : OrderedSpectrum M) (_γ : ℝ)
    (_hs : HierarchySpec M) (_hj : _hs.isJustified _spec _γ) :
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Hierarchy/EndogenousHierarchy.lean:432

Module Section

Endogenous Hierarchy: Network CES ↔ Spectral Hierarchy Bridge

In the same file