Documentation

Lean 4 Proof

theorem mpl_eq_laborShare_times_ypl {A α ρ : ℝ} (_hA : 0 < A)
    (hα : 0 < α) (hα1 : α < 1) (hρ : ρ ≠ 0)
    {K L : ℝ} (hK : 0 < K) (hL : 0 < L) :
    marginalProductL A α ρ K L =
    laborShare α ρ K L * (twoFactorCES A α ρ K L / L) := by
  simp only [marginalProductL, laborShare, 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 hL_ne : L ≠ 0 := ne_of_gt hL
  -- Rewrite L^{ρ-1} = L^ρ / L and I^{(1-ρ)/ρ} = I^{1/ρ} / I
  rw [show L ^ (ρ - 1) = L ^ ρ / L from rpow_sub_one hL_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

Location

thesis/CESProofs/Macro/TwoFactorCES.lean:256

Module Section

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

In the same file