Documentation

Lean 4 Proof

theorem twoFactorCES_pos {A α ρ : ℝ} (hA : 0 < A)
    (hα : 0 < α) (hα1 : α < 1) (_hρ : ρ ≠ 0)
    {K L : ℝ} (hK : 0 < K) (hL : 0 < L) :
    0 < twoFactorCES A α ρ K L := by
  simp only [twoFactorCES]
  exact mul_pos hA (rpow_pos_of_pos (cesInner_pos hα hα1 hK hL) (1 / ρ))

Dependency Graph

Used by

Location

thesis/CESProofs/Macro/TwoFactorCES.lean:129

Module Section

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

In the same file