Documentation

Lean 4 Proof

structure HierarchySpec (M : ℕ) where
  levels : ℕ
  hlevels : 0 < levels
  /-- Number of gaps = levels - 1. -/
  numGaps : ℕ
  hng : numGaps + 1 = levels
  /-- Gap positions (sorted, in {0, ..., M-2}). -/
  gapPositions : Fin numGaps → ℕ
  hgapBound : ∀ i, gapPositions i + 1 < M
  hgapSorted : StrictMono gapPositions

Dependency Graph

Used by

Location

thesis/CESProofs/Hierarchy/SpectralHierarchy.lean:128

Module Section

Endogenous Hierarchy: Why N Levels?

In the same file