Documentation

Lean 4 Proof

theorem irrelevance_test :
    -- Adding micro covariates beyond (rho, T, ell) should not
    -- improve macro-level forecasting R^2
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Dynamics/PolicyCost.lean:233

Module Section

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

In the same file