Sections / Section 13: Hierarchical Architecture / effective_rho_from_clustering

Effective Rho From Clustering

theoremtrivialHierarchy

Documentation

Lean 4 Proof

theorem effective_rho_from_clustering
    {M : ℕ} (_spec : OrderedSpectrum M) :
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Hierarchy/EndogenousHierarchy.lean:461

Module Section

Endogenous Hierarchy: Network CES ↔ Spectral Hierarchy Bridge

In the same file

HierarchicalPartition intraLevelQF interLevelQF qf_decomposition intraLevelQF_nonneg interLevelQF_nonneg single_level_inter_zero isDisconnected disconnected_inter_zero isNearDecomposable near_decomposable_pointwise network_hierarchy_bridge intra_bounded_by_total levelSize levelCoupling effectiveLevelCurvature effectiveLevelCurvature_nonneg effectiveLevelRho crossLevelDistQF crossLevelDistQF_nonneg