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

Capital Accumulation Eq Zero Iff

theoremprovedMacroeconomics

Documentation

Lean 4 Proof

theorem capitalAccumulation_eq_zero_iff {s δ Y K : ℝ} :
    capitalAccumulation s δ Y K = 0 ↔ s * Y = δ * K := by
  simp only [capitalAccumulation]; constructor <;> intro h <;> linarith

Dependency Graph

Used by

solowSteadyState_capitalShare tax_lowers_investment goldenRule_savings_eq_capitalShare steadyState_consumption_eq steadyState_KY_eq

Location

thesis/CESProofs/Macro/Accumulation.lean:74

Module Section

Accumulation Dynamics (Layer 2 of Macro Extension)

In the same file

capitalAccumulation eulerConsumptionGrowth afterTaxReturn steadyStateKY eulerSteadyStateReturn eulerSteadyStateMPK steadyStateConsumption 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