Documentation

Lean 4 Proof

def isStrictHierarchy {M N : ℕ} (w : Fin M → Fin N → ℝ) : Prop :=
  ∀ j n, w j n = 0 ∨ w j n = 1

Dependency Graph

Location

thesis/CESProofs/Hierarchy/SpectralHierarchy.lean:321

Module Section

Endogenous Hierarchy: Why N Levels?

In the same file