Documentation

Lean 4 Proof

theorem eulerConsumptionGrowth_pos_iff {γ τ_K r ρ_time : ℝ} (hγ : 0 < γ) :
    0 < eulerConsumptionGrowth γ τ_K r ρ_time ↔
    ρ_time < (1 - τ_K) * r := by
  simp only [eulerConsumptionGrowth]
  have hg : (0 : ℝ) < 1 / γ := div_pos one_pos hγ
  constructor
  · intro h
    -- (1/γ) * x > 0, with 1/γ > 0, so x > 0
    by_contra h_neg
    push_neg at h_neg
    have : (1 - τ_K) * r - ρ_time ≤ 0 := by linarith
    have := mul_nonpos_of_nonneg_of_nonpos (le_of_lt hg) this
    linarith
  · intro h
    exact mul_pos hg (by linarith)

Dependency Graph

Location

thesis/CESProofs/Macro/Accumulation.lean:160

Module Section

Accumulation Dynamics (Layer 2 of Macro Extension)

In the same file