Documentation

Lean 4 Proof

def HierarchySpec.isJustified (hs : HierarchySpec M) (spec : OrderedSpectrum M)
    (γ : ℝ) : Prop :=
  ∀ i : Fin hs.numGaps,
    γ < spec.gap ⟨hs.gapPositions i, by have := hs.hgapBound i; omega⟩
      (hs.hgapBound i)

Dependency Graph

Location

thesis/CESProofs/Hierarchy/SpectralHierarchy.lean:141

Module Section

Endogenous Hierarchy: Why N Levels?

In the same file