Documentation

Lean 4 Proof

theorem mp_ratio {A α ρ K L : ℝ} (_hA : 0 < A)
    (hα : 0 < α) (hα1 : α < 1) {_hρ : ρ ≠ 0}
    (hK : 0 < K) (hL : 0 < L) :
    marginalProductK A α ρ K L / marginalProductL A α ρ K L =
    (α / (1 - α)) * (K / L) ^ (ρ - 1) := by
  simp only [marginalProductK, marginalProductL]
  have hI_pos : 0 < (cesInner α ρ K L) ^ ((1 - ρ) / ρ) :=
    rpow_pos_of_pos (cesInner_pos hα hα1 hK hL) _
  have h1α : (0 : ℝ) < 1 - α := by linarith
  -- Cancel common factors A and I^{(1-ρ)/ρ}
  rw [show A * α * K ^ (ρ - 1) * (cesInner α ρ K L) ^ ((1 - ρ) / ρ) /
      (A * (1 - α) * L ^ (ρ - 1) * (cesInner α ρ K L) ^ ((1 - ρ) / ρ)) =
      (α / (1 - α)) * (K ^ (ρ - 1) / L ^ (ρ - 1)) from by
    field_simp]
  rw [div_rpow (le_of_lt hK) (le_of_lt hL)]

Dependency Graph

Used by

Location

thesis/CESProofs/Macro/TwoFactorCES.lean:282

Module Section

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

In the same file