theorem shephards_lemma {J : ℕ} (hJ : 0 < J) {ρ : ℝ} (hρ : ρ ≠ 0) (hρ1 : ρ ≠ 1)
{p : Fin J → ℝ} (hp : ∀ j, 0 < p j) (k : Fin J) :
HasDerivAt (fun t => cesUnitCost J ρ (Function.update p k t))
(cesDemand J ρ p k 1) (p k) := by
simp only [cesUnitCost, cesPriceIndex, cesDemand, unnormCES, dualExponent]
set r := ρ / (ρ - 1)
have hr : r ≠ 0 := div_ne_zero hρ (sub_ne_zero.mpr hρ1)
set S := ∑ j : Fin J, (p j) ^ r
set C := ∑ j ∈ Finset.univ.erase k, (p j) ^ r
have hSpk : (p k) ^ r + C = S := by
simp only [S, C]
have h := Finset.sum_erase_add Finset.univ (fun j => (p j) ^ r) (Finset.mem_univ k)
linarith
have hSpos : 0 < S := by
simp only [S]
exact Finset.sum_pos (fun j _ => rpow_pos_of_pos (hp j) r)
⟨⟨0, hJ⟩, Finset.mem_univ _⟩
-- Rewrite the function: updating p k to t gives inner sum = t^r + C
have hfun_eq : (fun t : ℝ =>
(∑ j : Fin J, (Function.update p k t j) ^ r) ^ (1 / r)) =
(fun t => (t ^ r + C) ^ (1 / r)) := funext (fun t => by
congr 1
conv_lhs => rw [← Finset.insert_erase (Finset.mem_univ k)]
rw [Finset.sum_insert (Finset.notMem_erase k _)]
simp only [Function.update_self]; congr 1
apply Finset.sum_congr rfl; intro j hj
simp [Function.update_of_ne ((Finset.mem_erase.mp hj).1)])
rw [hfun_eq]
-- Inner derivative: d/dt [t^r + C] = r * t^{r-1}
have hAd : HasDerivAt (fun t : ℝ => t ^ r + C)
(r * (p k) ^ (r - 1)) (p k) := by
have h := (hasDerivAt_id (p k)).rpow_const (p := r) (Or.inl (hp k).ne')
simp only [id, one_mul] at h
exact h.add_const C
-- Chain rule: d/dt [(t^r + C)^{1/r}]
have h_rpow := hAd.rpow_const (p := 1 / r) (Or.inl (hSpk ▸ hSpos).ne')
have hOuter := hSpk ▸ h_rpow
-- Algebraic identity: chain rule derivative = cesDemand form
have hkey : r * (p k) ^ (r - 1) * (1 / r) * S ^ (1 / r - 1) =
1 * (p k) ^ (r - 1) * (S ^ (1 / r)) ^ (1 - r) := by
rw [← Real.rpow_mul (le_of_lt hSpos)]
have h1 : 1 / r * (1 - r) = 1 / r - 1 := by field_simp [hr]
rw [h1]
have h2 : r * (p k) ^ (r - 1) * (1 / r) = 1 * (p k) ^ (r - 1) := by
field_simp [hr]
rw [h2]
exact hkey ▸ hOuterEconomics extensions for CES formalization: