Documentation

Lean 4 Proof

theorem single_level_always_justified (M : ℕ) (spec : OrderedSpectrum M) (γ : ℝ) :
    (⟨1, one_pos, 0, rfl, Fin.elim0, fun i => Fin.elim0 i,
      fun i => Fin.elim0 i⟩ : HierarchySpec M).isJustified spec γ := by
  intro i; exact Fin.elim0 i

Dependency Graph

Location

thesis/CESProofs/Hierarchy/SpectralHierarchy.lean:151

Module Section

Endogenous Hierarchy: Why N Levels?

In the same file