Documentation

Lean 4 Proof

theorem no_large_gap_single_level {M : ℕ} (spec : OrderedSpectrum M)
    (γ : ℝ) (_hγ : 1 < γ)
    (hnoGap : ∀ (k : Fin M) (hk : (k : ℕ) + 1 < M), spec.gap k hk ≤ γ)
    (hs : HierarchySpec M) (hN : 1 ≤ hs.numGaps)
    (hj : hs.isJustified spec γ) : False := by
  have i : Fin hs.numGaps := ⟨0, hN⟩
  have hgap := hj i
  have hbnd := hs.hgapBound i
  have hbound := hnoGap ⟨hs.gapPositions i, by omega⟩ hbnd
  linarith

Dependency Graph

Location

thesis/CESProofs/Hierarchy/SpectralHierarchy.lean:165

Module Section

Endogenous Hierarchy: Why N Levels?

In the same file