Euler Consumption Growth

def proved Macroeconomics

Documentation

Lean 4 Proof

def eulerConsumptionGrowth (γ τ_K r ρ_time : ℝ) : ℝ :=
  (1 / γ) * ((1 - τ_K) * r - ρ_time)

Dependency Graph

Used by

eulerConsumptionGrowth_decreasing_in_τ eulerConsumptionGrowth_pos_iff ramseySteadyState_MPK eulerConsumptionGrowth_eq_zero_iff eulerSteadyState_r_eq eulerConsumptionGrowth_increasing_in_r

Location

thesis/CESProofs/Macro/Accumulation.lean:41

Module Section

Accumulation Dynamics (Layer 2 of Macro Extension)