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

Steady State Ky Pos

theoremprovedMacroeconomics

Documentation

Lean 4 Proof

theorem steadyStateKY_pos {s δ : ℝ} (hs : 0 < s) (hδ : 0 < δ) :
    0 < steadyStateKY s δ := by
  simp only [steadyStateKY]; exact div_pos hs hδ

Dependency Graph

Location

thesis/CESProofs/Macro/Accumulation.lean:92

Module Section

Accumulation Dynamics (Layer 2 of Macro Extension)

In the same file

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