Documentation

Lean 4 Proof

theorem OrderedSpectrum.gap_ge_one (spec : OrderedSpectrum M) (k : Fin M)
    (hk : (k : ℕ) + 1 < M) :
    1 ≤ spec.gap k hk := by
  unfold OrderedSpectrum.gap
  rw [le_div_iff₀ (spec.pos ⟨(k : ℕ) + 1, hk⟩), one_mul]
  exact spec.mono (Fin.mk_le_mk.mpr (Nat.le_succ _))

Dependency Graph

Location

thesis/CESProofs/Hierarchy/SpectralHierarchy.lean:100

Module Section

Endogenous Hierarchy: Why N Levels?

In the same file