Documentation

Lean 4 Proof

theorem aggregation_rhoT (J : ℕ) (rho T Tstar : ℝ) :
    -- K_macro = K_micro · max(0, 1 - T/T*)
    effectiveCurvatureKeff J rho T Tstar =
    curvatureK J rho * max 0 (1 - T / Tstar) := by rfl

Dependency Graph

Location

thesis/CESProofs/Dynamics/PolicyCost.lean:166

Module Section

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

In the same file