Documentation

Lean 4 Proof

theorem ces_demand_adding_up {J : ℕ} (hJ : 0 < J) {ρ : ℝ} (hρ : ρ ≠ 0) (hρ1 : ρ ≠ 1)
    {p : Fin J → ℝ} (hp : ∀ j, 0 < p j) (y : ℝ) :
    ∑ k : Fin J, p k * cesDemand J ρ p k y = cesUnitCost J ρ p * y := by
  simp only [cesDemand, cesUnitCost, cesPriceIndex, 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
  have hSpos : 0 < S := Finset.sum_pos (fun j _ => rpow_pos_of_pos (hp j) r)
    ⟨⟨0, hJ⟩, Finset.mem_univ _⟩
  -- Each term: p k * (y * (p k)^{r-1} * (S^{1/r})^{1-r}) = y * (S^{1/r})^{1-r} * (p k)^r
  have hterm : ∀ k : Fin J,
      p k * (y * (p k) ^ (r - 1) * (S ^ (1 / r)) ^ (1 - r)) =
      y * (S ^ (1 / r)) ^ (1 - r) * (p k) ^ r := by
    intro k
    have hpk : p k * (p k) ^ (r - 1) = (p k) ^ r := by
      have h := rpow_add (hp k) 1 (r - 1)
      rw [rpow_one, show 1 + (r - 1) = r from by ring] at h; exact h.symm
    rw [show p k * (y * (p k) ^ (r - 1) * (S ^ (1 / r)) ^ (1 - r)) =
        y * (S ^ (1 / r)) ^ (1 - r) * (p k * (p k) ^ (r - 1)) from by ring]
    rw [hpk]
  simp_rw [hterm, ← Finset.mul_sum]
  -- Goal: y * (S^{1/r})^{1-r} * S = S^{1/r} * y
  rw [← rpow_mul (le_of_lt hSpos)]
  -- Combine: S^{a} * S = S^{a+1} where a = 1/r*(1-r)
  have key : S ^ (1 / r * (1 - r)) * S = S ^ (1 / r) := by
    have h := rpow_add hSpos (1 / r * (1 - r)) 1
    rw [rpow_one, show 1 / r * (1 - r) + 1 = 1 / r from by field_simp [hr]; ring] at h
    exact h.symm
  have : y * S ^ (1 / r * (1 - r)) * S = y * (S ^ (1 / r * (1 - r)) * S) := by ring
  rw [this, key]; ring

Dependency Graph

Location

thesis/CESProofs/Applications/Economics.lean:966

Module Section

Economics extensions for CES formalization:

In the same file