Aggregation-Invariant Classes

theorem trivial Dynamics & Crises

Documentation

Lean 4 Proof

theorem aggregation_invariant_classes :
    -- Three fixed points: rho = 0, rho -> 1, rho -> -infinity
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Dynamics/PolicyCost.lean:187

Module Section

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

In the same file

jarzynski_equality policy_cost_bound friction_work_nonneg friction_work_estimate optimalPolicyTimescale optimalPolicyTimescale_pos aggregation_rhoT macroscopic_predictability irrelevance_test policy_cost_scales_with_T