Documentation

Lean 4 Proof

theorem cesPriceIndex_eq_sigma {ρ : ℝ} (hρ1 : ρ ≠ 1) {p : Fin J → ℝ} :
    cesPriceIndex J ρ p =
    (∑ j : Fin J, (p j) ^ (1 - elasticityOfSubstitution ρ)) ^
      (1 / (1 - elasticityOfSubstitution ρ)) := by
  simp only [cesPriceIndex, unnormCES]
  congr 1
  · apply Finset.sum_congr rfl; intro j _
    congr 1; exact dualExponent_eq_sigma hρ1
  · congr 1; exact dualExponent_eq_sigma hρ1

Dependency Graph

Location

thesis/CESProofs/Applications/Economics.lean:515

Module Section

Economics extensions for CES formalization:

In the same file