Documentation

Lean 4 Proof

theorem ramsey_dynamicallyEfficient {τ_K ρ_time g : ℝ}
    (hτ : τ_K < 1) (hρg : (1 - τ_K) * g < ρ_time) :
    dynamicallyEfficient (eulerSteadyStateReturn τ_K ρ_time) g := by
  simp only [dynamicallyEfficient, eulerSteadyStateReturn, gt_iff_lt]
  have h1τ : (0 : ℝ) < 1 - τ_K := by linarith
  rw [lt_div_iff₀ h1τ]
  rw [mul_comm] at hρg ⊢
  linarith

Dependency Graph

Location

thesis/CESProofs/Macro/Accumulation.lean:331

Module Section

Accumulation Dynamics (Layer 2 of Macro Extension)

In the same file