Documentation

Lean 4 Proof

theorem macroscopic_predictability :
    -- Macro dynamics depend only on (rho, T, ell)
    -- All micro-level heterogeneity is integrated out
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Dynamics/PolicyCost.lean:211

Module Section

Results 26-35: Minimum Policy Cost and Multi-Scale Aggregation

In the same file