Documentation

Lean 4 Proof

def cesDemand (J : ℕ) (ρ : ℝ) (p : Fin J → ℝ) (k : Fin J) (y : ℝ) : ℝ :=
  y * (p k) ^ (ρ / (ρ - 1) - 1) * (cesUnitCost J ρ p) ^ (1 - ρ / (ρ - 1))

Dependency Graph

Used by

Location

thesis/CESProofs/Applications/Economics.lean:910

Module Section

Economics extensions for CES formalization:

In the same file