Documentation

Lean 4 Proof

theorem ramseySteadyState_MPK {γ τ_K ρ_time δ MPK : ℝ} (hγ : γ ≠ 0)
    (hτ : τ_K < 1)
    (heuler : eulerConsumptionGrowth γ τ_K (MPK - δ) ρ_time = 0) :
    MPK = eulerSteadyStateMPK τ_K ρ_time δ := by
  have hr := eulerSteadyState_r_eq hγ hτ heuler
  simp only [eulerSteadyStateReturn] at hr
  simp only [eulerSteadyStateMPK]
  linarith

Dependency Graph

Location

thesis/CESProofs/Macro/Accumulation.lean:277

Module Section

Accumulation Dynamics (Layer 2 of Macro Extension)

In the same file