Documentation

Lean 4 Proof

theorem goldenRule_savings_eq_capitalShare {A α ρ s δ : ℝ} (hA : 0 < A)
    (hα : 0 < α) (hα1 : α < 1) (hρ : ρ ≠ 0) (_hs : 0 < s) (_hδ : 0 < δ)
    {K L : ℝ} (hK : 0 < K) (hL : 0 < L)
    (hss : capitalAccumulation s δ (twoFactorCES A α ρ K L) K = 0)
    (hgr : marginalProductK A α ρ K L = δ) :
    s = capitalShare α ρ K L := by
  -- From mpk = s_K * Y/K and mpk = δ and s*Y = δ*K (SS):
  -- s_K * Y/K = δ → s_K * Y = δ*K = s*Y → s_K = s
  have hY := twoFactorCES_pos hA hα hα1 hρ hK hL
  have hY_ne := ne_of_gt hY
  have hK_ne := ne_of_gt hK
  have hmk := mpk_eq_capitalShare_times_ypk (show 0 < A from hA) hα hα1 hρ hK hL
  have h_eq := capitalAccumulation_eq_zero_iff.mp hss
  -- hmk: MPK = s_K * (Y / K)
  -- hgr: MPK = δ
  -- h_eq: s * Y = δ * K
  -- So s_K * (Y/K) = δ → s_K * Y = δ * K = s * Y → s_K = s
  rw [hgr] at hmk
  -- hmk: δ = s_K * (Y / K) → s_K * Y = δ * K
  have h1 : capitalShare α ρ K L * twoFactorCES A α ρ K L = δ * K := by
    have := hmk; field_simp at this; linarith
  -- s * Y = δ * K = s_K * Y, so s = s_K
  have h2 : s * twoFactorCES A α ρ K L =
      capitalShare α ρ K L * twoFactorCES A α ρ K L := by linarith
  exact mul_right_cancel₀ hY_ne h2

Dependency Graph

Used by

Location

thesis/CESProofs/Macro/Accumulation.lean:229

Module Section

Accumulation Dynamics (Layer 2 of Macro Extension)

In the same file