Documentation

Lean 4 Proof

theorem steadyState_KY_eq {s δ Y K : ℝ} (hδ : 0 < δ) (hY : 0 < Y)
    (hss : capitalAccumulation s δ Y K = 0) :
    K / Y = steadyStateKY s δ := by
  simp only [steadyStateKY]
  have h := capitalAccumulation_eq_zero_iff.mp hss
  -- s * Y = δ * K → K/Y = s/δ
  have hY_ne := ne_of_gt hY
  have hδ_ne := ne_of_gt hδ
  rw [div_eq_div_iff hY_ne hδ_ne]
  linarith

Dependency Graph

Location

thesis/CESProofs/Macro/Accumulation.lean:80

Module Section

Accumulation Dynamics (Layer 2 of Macro Extension)

In the same file