Documentation

Lean 4 Proof

theorem mpk_eq_capitalShare_times_ypk {A α ρ : ℝ} (_hA : 0 < A)
    (hα : 0 < α) (hα1 : α < 1) (hρ : ρ ≠ 0)
    {K L : ℝ} (hK : 0 < K) (hL : 0 < L) :
    marginalProductK A α ρ K L =
    capitalShare α ρ K L * (twoFactorCES A α ρ K L / K) := by
  simp only [marginalProductK, capitalShare, twoFactorCES, cesInner]
  set I := α * K ^ ρ + (1 - α) * L ^ ρ
  have hI_pos : 0 < I := cesInner_pos hα hα1 hK hL
  have hI_ne : I ≠ 0 := ne_of_gt hI_pos
  have hK_ne : K ≠ 0 := ne_of_gt hK
  -- Rewrite K^{ρ-1} = K^ρ / K and I^{(1-ρ)/ρ} = I^{1/ρ} / I
  rw [show K ^ (ρ - 1) = K ^ ρ / K from rpow_sub_one hK_ne ρ]
  rw [show I ^ ((1 - ρ) / ρ) = I ^ (1 / ρ) / I from by
    rw [show (1 - ρ) / ρ = 1 / ρ - 1 from by field_simp]
    exact rpow_sub_one hI_ne (1 / ρ)]
  field_simp

Dependency Graph

Used by

Location

thesis/CESProofs/Macro/TwoFactorCES.lean:238

Module Section

Two-Factor CES Production Function (Layer 1 of Macro Extension)

In the same file