Documentation

Lean 4 Proof

theorem twoFactorCES_symmetric {A α ρ : ℝ} (_hA : 0 < A)
    (hα : 0 < α) (hα1 : α < 1) (hρ : ρ ≠ 0)
    {x : ℝ} (hx : 0 < x) :
    twoFactorCES A α ρ x x = A * x := by
  simp only [twoFactorCES]
  rw [cesInner_symmetric hα hα1]
  rw [← rpow_mul (le_of_lt hx), mul_one_div_cancel hρ, rpow_one]

Dependency Graph

Location

thesis/CESProofs/Macro/TwoFactorCES.lean:406

Module Section

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

In the same file