Documentation

Lean 4 Proof

theorem cesInner_scale {α ρ K L : ℝ} {c : ℝ} (hc : 0 < c)
    (hK : 0 < K) (hL : 0 < L) :
    cesInner α ρ (c * K) (c * L) = c ^ ρ * cesInner α ρ K L := by
  simp only [cesInner]
  rw [mul_rpow (le_of_lt hc) (le_of_lt hK),
      mul_rpow (le_of_lt hc) (le_of_lt hL)]
  ring

Dependency Graph

Used by

Location

thesis/CESProofs/Macro/TwoFactorCES.lean:93

Module Section

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

In the same file