Documentation

Lean 4 Proof

theorem ramsey_above_goldenRule {τ_K ρ_time δ : ℝ}
    (hρ : 0 < ρ_time) (hτ : τ_K < 1) :
    δ < eulerSteadyStateMPK τ_K ρ_time δ := by
  simp only [eulerSteadyStateMPK]
  have h := eulerSteadyStateReturn_pos hρ hτ
  simp only [eulerSteadyStateReturn] at h
  linarith

Dependency Graph

Location

thesis/CESProofs/Macro/Accumulation.lean:304

Module Section

Accumulation Dynamics (Layer 2 of Macro Extension)

In the same file