Documentation

Lean 4 Proof

def OrderedSpectrum.gap (spec : OrderedSpectrum M) (k : Fin M)
    (hk : (k : ℕ) + 1 < M) : ℝ :=
  spec.rate k / spec.rate ⟨(k : ℕ) + 1, hk⟩

Dependency Graph

Location

thesis/CESProofs/Hierarchy/SpectralHierarchy.lean:93

Module Section

Endogenous Hierarchy: Why N Levels?

In the same file