Documentation

Lean 4 Proof

theorem dynamicEfficiency_below_goldenRule {MPK δ : ℝ} (hMPK : δ < MPK) :
    dynamicallyEfficient (MPK - δ) 0 := by
  simp only [dynamicallyEfficient]; linarith

Dependency Graph

Location

thesis/CESProofs/Macro/Accumulation.lean:342

Module Section

Accumulation Dynamics (Layer 2 of Macro Extension)

In the same file