Documentation

Lean 4 Proof

theorem structural_invariant_convergence_speed
    (e : HierarchicalCESEconomy N) (n : Fin N) :
    0 < convergenceSpeed e n :=
  convergenceSpeed_pos e n

Dependency Graph

Location

thesis/CESProofs/Hierarchy/ModuliSpace.lean:49

Module Section

Theorems 3-4: Structural Determination and Endogenous Hierarchy Depth

In the same file