Documentation

Lean 4 Proof

theorem capitalShare_eq_factorShare {α ρ K L : ℝ} :
    capitalShare α ρ K L =
    factorShare 2 (fun j => if j = ⟨0, by omega⟩ then α else 1 - α) ρ
      (fun j => if j = ⟨0, by omega⟩ then K else L) ⟨0, by omega⟩ := by
  simp only [capitalShare, factorShare, cesInner]
  congr 1 <;> simp [Fin.sum_univ_two]

Dependency Graph

Location

thesis/CESProofs/Macro/TwoFactorCES.lean:367

Module Section

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

In the same file