Documentation

Lean 4 Proof

theorem steadyState_consumption_eq {s δ Y K : ℝ} (_hY : 0 < Y)
    (hss : capitalAccumulation s δ Y K = 0) :
    Y - δ * K = (1 - s) * Y := by
  have h := capitalAccumulation_eq_zero_iff.mp hss
  linarith

Dependency Graph

Location

thesis/CESProofs/Macro/Accumulation.lean:208

Module Section

Accumulation Dynamics (Layer 2 of Macro Extension)

In the same file