Documentation

Lean 4 Proof

theorem cesPriceIndex_def {ρ : ℝ} (_hρ : ρ ≠ 0) (_hρ1 : ρ ≠ 1)
    {p : Fin J → ℝ} :
    cesPriceIndex J ρ p = (∑ j : Fin J, (p j) ^ (ρ / (ρ - 1))) ^ (1 / (ρ / (ρ - 1))) := by
  simp only [cesPriceIndex, unnormCES, dualExponent]

Dependency Graph

Location

thesis/CESProofs/Applications/Economics.lean:508

Module Section

Economics extensions for CES formalization:

In the same file