Documentation

Lean 4 Proof

theorem twoFactorCES_homogDegOne {A α ρ : ℝ} (_hA : 0 < A)
    (hα : 0 < α) (hα1 : α < 1) (hρ : ρ ≠ 0)
    {K L : ℝ} (hK : 0 < K) (hL : 0 < L) {c : ℝ} (hc : 0 < c) :
    twoFactorCES A α ρ (c * K) (c * L) = c * twoFactorCES A α ρ K L := by
  simp only [twoFactorCES]
  rw [cesInner_scale hc hK hL]
  rw [mul_rpow (rpow_nonneg (le_of_lt hc) ρ) (cesInner_nonneg hα hα1 hK hL)]
  rw [← rpow_mul (le_of_lt hc), mul_one_div_cancel hρ, rpow_one]
  ring

Dependency Graph

Used by

Location

thesis/CESProofs/Macro/TwoFactorCES.lean:118

Module Section

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

In the same file