Documentation

Lean 4 Proof

theorem welfare_lyapunov_dissipation (e : HierarchicalCESEconomy N) :
    -- dV/dt ≤ 0 along the hierarchical dynamics
    -- The cross-level terms cancel due to the graph-Lyapunov
    -- construction of Li, Shuai, and van den Driessche
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Hierarchy/WelfareDecomposition.lean:77

Module Section

Theorems 7-8, Propositions 5 and 7, Corollary 3:

In the same file