Sections / Section 13: Hierarchical Architecture / OrderedSpectrum

Ordered Spectrum

structureprovedHierarchy

Documentation

Lean 4 Proof

structure OrderedSpectrum (M : ℕ) where
  rate : Fin M → ℝ
  pos : ∀ i, 0 < rate i
  mono : Antitone rate

Dependency Graph

Used by

HierarchySpec.isJustified spectral_hierarchy_justifies_N OrderedSpectrum.gap single_level_always_justified OrderedSpectrum.gap_ge_one optimal_N_spectral total_spread_eq_endpoint_ratio north_institutional_layering effective_rho_from_clustering no_large_gap_single_level eigenvalue_clustering_partition

Location

thesis/CESProofs/Hierarchy/SpectralHierarchy.lean:87

Module Section

Endogenous Hierarchy: Why N Levels?

In the same file

adjustmentRate timescaleFromRate spectralGapRatio timescale_ratio_eq_rate_ratio large_gap_implies_separation OrderedSpectrum.gap OrderedSpectrum.gap_ge_one total_spread_eq_endpoint_ratio HierarchySpec HierarchySpec.isJustified single_level_always_justified no_large_gap_single_level nearDecomposabilityParam simon_near_decomposable_gap decomposability_monotone crossBlockCoupling transaction_cost_reduces_coupling williamson_hierarchy_creation north_institutional_layering overlapWeight