Documentation

Lean 4 Proof

theorem onsager_testable (e : NSectorEconomy N) :
    -- Cross-sector impulse responses should be symmetric
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Dynamics/SymmetricAdjustment.lean:65

Module Section

Results 17-25: Symmetric Adjustment and Transition Rates

In the same file