Documentation

Lean 4 Proof

theorem euler_two_factor {A α ρ : ℝ} (_hA : 0 < A)
    (hα : 0 < α) (hα1 : α < 1) (hρ : ρ ≠ 0)
    {K L : ℝ} (hK : 0 < K) (hL : 0 < L) :
    marginalProductK A α ρ K L * K + marginalProductL A α ρ K L * L =
    twoFactorCES A α ρ K L := by
  simp only [marginalProductK, marginalProductL, twoFactorCES, cesInner]
  set I := α * K ^ ρ + (1 - α) * L ^ ρ with hI_def
  -- Combine x^{ρ-1} · x = x^ρ
  have hK_combine : K ^ (ρ - 1) * K = K ^ ρ := by
    have h := rpow_add hK (ρ - 1) 1
    rw [rpow_one, show ρ - 1 + 1 = ρ from by ring] at h; exact h.symm
  have hL_combine : L ^ (ρ - 1) * L = L ^ ρ := by
    have h := rpow_add hL (ρ - 1) 1
    rw [rpow_one, show ρ - 1 + 1 = ρ from by ring] at h; exact h.symm
  -- Rearrange LHS
  have step1 : A * α * K ^ (ρ - 1) * I ^ ((1 - ρ) / ρ) * K +
      A * (1 - α) * L ^ (ρ - 1) * I ^ ((1 - ρ) / ρ) * L =
      A * I ^ ((1 - ρ) / ρ) * (α * K ^ ρ + (1 - α) * L ^ ρ) := by
    have lhs_rw1 : A * α * K ^ (ρ - 1) * I ^ ((1 - ρ) / ρ) * K =
        A * (α * (K ^ (ρ - 1) * K)) * I ^ ((1 - ρ) / ρ) := by ring
    have lhs_rw2 : A * (1 - α) * L ^ (ρ - 1) * I ^ ((1 - ρ) / ρ) * L =
        A * ((1 - α) * (L ^ (ρ - 1) * L)) * I ^ ((1 - ρ) / ρ) := by ring
    rw [lhs_rw1, lhs_rw2, hK_combine, hL_combine]; ring
  rw [step1, ← hI_def]
  -- I^{(1-ρ)/ρ} · I = I^{1/ρ}
  have hI_pos : 0 < I := by rw [hI_def]; exact cesInner_pos hα hα1 hK hL
  rw [show A * I ^ ((1 - ρ) / ρ) * I = A * (I ^ ((1 - ρ) / ρ) * I) from by ring]
  congr 1
  -- I^{(1-ρ)/ρ} * I = I^{1/ρ}
  have h1 : I ^ ((1 - ρ) / ρ + 1) = I ^ ((1 - ρ) / ρ) * I ^ (1 : ℝ) :=
    rpow_add hI_pos _ _
  rw [rpow_one] at h1
  rw [← h1]
  congr 1; field_simp; ring

Dependency Graph

Used by

Location

thesis/CESProofs/Macro/TwoFactorCES.lean:197

Module Section

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

In the same file