Documentation

Lean 4 Proof

theorem eulerConsumptionGrowth_increasing_in_r {γ τ_K r₁ r₂ ρ_time : ℝ}
    (hγ : 0 < γ) (_hτ : τ_K < 1) (hr : r₁ < r₂) :
    eulerConsumptionGrowth γ τ_K r₁ ρ_time <
    eulerConsumptionGrowth γ τ_K r₂ ρ_time := by
  simp only [eulerConsumptionGrowth]
  have hg : (0 : ℝ) < 1 / γ := div_pos one_pos hγ
  apply mul_lt_mul_of_pos_left _ hg
  nlinarith

Dependency Graph

Location

thesis/CESProofs/Macro/Accumulation.lean:407

Module Section

Accumulation Dynamics (Layer 2 of Macro Extension)

In the same file