Euler Steady State Mpk

def proved Macroeconomics

Documentation

Lean 4 Proof

def eulerSteadyStateMPK (τ_K ρ_time δ : ℝ) : ℝ := ρ_time / (1 - τ_K) + δ

Dependency Graph

Used by

ramseySteadyState_MPK higherTax_higherRequiredReturn eulerSteadyStateMPK_zero_tax tax_wedge_on_MPK ramsey_goldenRule_wedge tax_wedge_pos zeroTax_minimizes_requiredMPK eulerSteadyStateMPK_eq ramsey_above_goldenRule eulerSteadyStateMPK_increasing_in_τ

Location

thesis/CESProofs/Macro/Accumulation.lean:63

Module Section

Accumulation Dynamics (Layer 2 of Macro Extension)