Documentation

Lean 4 Proof

theorem eulerConsumptionGrowth_eq_zero_iff {γ τ_K r ρ_time : ℝ} (hγ : γ ≠ 0) :
    eulerConsumptionGrowth γ τ_K r ρ_time = 0 ↔
    (1 - τ_K) * r = ρ_time := by
  simp only [eulerConsumptionGrowth]
  have h1g : (1 : ℝ) / γ ≠ 0 := div_ne_zero one_ne_zero hγ
  constructor
  · intro h
    have := (mul_eq_zero.mp h).resolve_left h1g
    linarith
  · intro h
    have : (1 - τ_K) * r - ρ_time = 0 := by linarith
    rw [this, mul_zero]

Dependency Graph

Used by

Location

thesis/CESProofs/Macro/Accumulation.lean:118

Module Section

Accumulation Dynamics (Layer 2 of Macro Extension)

In the same file