Lean 4 Proof

theorem laborShare_lt_one {α ρ K L : ℝ}
    (hα : 0 < α) (hα1 : α < 1) (hK : 0 < K) (hL : 0 < L) :
    laborShare α ρ K L < 1 := by
  have hsum := capitalShare_plus_laborShare (ρ := ρ) hα hα1 hK hL
  have hK_pos := capitalShare_pos (ρ := ρ) hα hα1 hK hL
  linarith

Dependency Graph

Location

thesis/CESProofs/Macro/TwoFactorCES.lean:175

Module Section

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

In the same file