Documentation

Lean 4 Proof

theorem capitalShare_plus_laborShare {α ρ K L : ℝ}
    (hα : 0 < α) (hα1 : α < 1) (hK : 0 < K) (hL : 0 < L) :
    capitalShare α ρ K L + laborShare α ρ K L = 1 := by
  simp only [capitalShare, laborShare]
  rw [← add_div]
  exact div_self (ne_of_gt (cesInner_pos hα hα1 hK hL))

Dependency Graph

Used by

Location

thesis/CESProofs/Macro/TwoFactorCES.lean:143

Module Section

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

In the same file