Documentation

Lean 4 Proof

theorem twoFactorCES_eq_cesFun {A α ρ : ℝ}
    {K L : ℝ} :
    twoFactorCES A α ρ K L =
    A * cesFun 2 (fun j => if j = ⟨0, by omega⟩ then α else 1 - α) ρ
      (fun j => if j = ⟨0, by omega⟩ then K else L) := by
  simp only [twoFactorCES, cesFun, cesInner]
  congr 1; congr 1
  -- Show the sum over Fin 2 equals α·K^ρ + (1-α)·L^ρ
  rw [Fin.sum_univ_two]
  simp

Dependency Graph

Location

thesis/CESProofs/Macro/TwoFactorCES.lean:354

Module Section

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

In the same file