Documentation

Lean 4 Proof

theorem eulerSteadyState_r_eq {γ τ_K r ρ_time : ℝ} (hγ : γ ≠ 0)
    (hτ : τ_K < 1) (hss : eulerConsumptionGrowth γ τ_K r ρ_time = 0) :
    r = eulerSteadyStateReturn τ_K ρ_time := by
  simp only [eulerSteadyStateReturn]
  have h := (eulerConsumptionGrowth_eq_zero_iff hγ).mp hss
  have h1τ : (1 : ℝ) - τ_K ≠ 0 := ne_of_gt (by linarith)
  field_simp at h ⊢
  linarith

Dependency Graph

Used by

Location

thesis/CESProofs/Macro/Accumulation.lean:132

Module Section

Accumulation Dynamics (Layer 2 of Macro Extension)

In the same file