Sections / Section 13: Hierarchical Architecture / HierarchicalPartition

Hierarchical Partition

structureprovedHierarchy

Documentation

Lean 4 Proof

structure HierarchicalPartition (J : ℕ) (N : ℕ) where
  level : Fin J → Fin N
  nonempty_levels : ∀ n : Fin N, ∃ j : Fin J, level j = n

Dependency Graph

Used by

isNearDecomposable uniform_effectiveLevelCurvature_trivial levelCoupling hierarchy_is_spectral_decomposition interLevelQF hierarchy_approximation_quality effectiveLevelRho effectiveLevelCurvature_nonneg intraLevelQF_nonneg crossLevelDistQF_nonneg isDisconnected single_level_inter_zero uniform_levelCoupling_trivial intraLevelQF interLevelQF_nonneg network_hierarchy_bridge near_decomposable_intra_approximation disconnected_inter_zero uniform_effectiveLevelRho_trivial crossLevelDistQF near_decomposable_pointwise effectiveLevelCurvature intra_bounded_by_total qf_decomposition levelSize

Location

thesis/CESProofs/Hierarchy/EndogenousHierarchy.lean:47

Module Section

Endogenous Hierarchy: Network CES ↔ Spectral Hierarchy Bridge

In the same file

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 hierarchy_approximation_quality