Sections / Section 14: Macro -- Two-Factor CES, Growth, Tax / eulerSteadyStateReturn

Euler Steady State Return

defprovedMacroeconomics

Documentation

Lean 4 Proof

def eulerSteadyStateReturn (τ_K ρ_time : ℝ) : ℝ := ρ_time / (1 - τ_K)

Dependency Graph

Used by

eulerSteadyStateReturn_zero_tax ramsey_dynamicallyEfficient eulerSteadyStateReturn_increasing_in_τ ramseySteadyState_MPK tax_wedge_on_MPK eulerSteadyState_r_eq ramsey_goldenRule_wedge eulerSteadyStateReturn_pos eulerSteadyStateMPK_eq ramsey_above_goldenRule eulerSteadyStateMPK_increasing_in_τ

Location

thesis/CESProofs/Macro/Accumulation.lean:57

Module Section

Accumulation Dynamics (Layer 2 of Macro Extension)

In the same file

capitalAccumulation eulerConsumptionGrowth afterTaxReturn steadyStateKY eulerSteadyStateMPK steadyStateConsumption capitalAccumulation_eq_zero_iff steadyState_KY_eq steadyStateKY_pos steadyStateKY_increasing_in_s steadyStateKY_decreasing_in_δ eulerConsumptionGrowth_eq_zero_iff eulerSteadyState_r_eq eulerSteadyStateReturn_pos eulerSteadyStateReturn_increasing_in_τ eulerConsumptionGrowth_pos_iff afterTaxReturn_decreasing afterTaxReturn_zero_tax afterTaxReturn_full_tax afterTaxReturn_pos