Documentation

Lean 4 Proof

theorem solowSteadyState_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) :
    capitalShare α ρ K L = s * marginalProductK A α ρ K L / δ := by
  have hY := twoFactorCES_pos hA hα hα1 hρ hK hL
  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
  have hK_ne := ne_of_gt hK
  have hY_ne := ne_of_gt hY
  have hδ_ne := ne_of_gt hδ
  -- hmk: MPK = s_K * (Y / K)
  -- h_eq: s * Y = δ * K
  -- Goal: s_K = s * MPK / δ = s * (s_K * Y/K) / δ
  -- i.e., s_K * δ = s * s_K * Y/K
  -- i.e., s_K * δ * K = s * s_K * Y
  -- i.e., δ * K = s * Y  (dividing by s_K > 0)
  -- which is h_eq ✓
  rw [hmk]
  have hs_K := capitalShare_pos (ρ := ρ) hα hα1 hK hL
  field_simp
  nlinarith

Dependency Graph

Location

thesis/CESProofs/Macro/Accumulation.lean:356

Module Section

Accumulation Dynamics (Layer 2 of Macro Extension)

In the same file