Documentation

Lean 4 Proof

theorem euler_ces_algebraic {J : ℕ} (_hJ : 0 < J) {ρ : ℝ} (hρ : ρ ≠ 0)
    {x : Fin J → ℝ} (hx : ∀ j, 0 < x j) :
    ∑ k : Fin J, x k * cesGradComponent J ρ x k = powerMean J ρ hρ x := by
  simp only [cesGradComponent, powerMean]
  set A := (1 / ↑J : ℝ) * ∑ j : Fin J, (x j) ^ ρ with hA_def
  -- Step 1: x_k * (1/J) * x_k^{rho-1} * A^{...} = (1/J) * x_k^rho * A^{...}
  have h1 : ∀ k : Fin J,
      x k * ((1 / ↑J) * (x k) ^ (ρ - 1) * A ^ ((1 - ρ) / ρ)) =
      (1 / ↑J) * (x k) ^ ρ * A ^ ((1 - ρ) / ρ) := by
    intro k
    have hxk : 0 < x k := hx k
    have hrpow : x k * (x k) ^ (ρ - 1) = (x k) ^ ρ := by
      have h := rpow_add hxk 1 (ρ - 1)
      rw [show (1 : ℝ) + (ρ - 1) = ρ from by ring, rpow_one] at h
      exact h.symm
    have : x k * (1 / ↑J * (x k) ^ (ρ - 1) * A ^ ((1 - ρ) / ρ)) =
        1 / ↑J * (x k * (x k) ^ (ρ - 1)) * A ^ ((1 - ρ) / ρ) := by ring
    rw [this, hrpow]
  simp_rw [h1]
  -- Step 2: Factor A^{...} out of the sum
  rw [← Finset.sum_mul]
  -- Step 3: (1/J) Sum x_k^rho = A
  rw [← Finset.mul_sum]
  -- Step 4: A * A^{(1-rho)/rho} = A^{1/rho}
  have hA_pos : 0 < A := by
    apply mul_pos (div_pos one_pos (by exact_mod_cast _hJ : (0 : ℝ) < ↑J))
    exact Finset.sum_pos (fun j _ => rpow_pos_of_pos (hx j) ρ) ⟨⟨0, _hJ⟩, Finset.mem_univ _⟩
  calc A * A ^ ((1 - ρ) / ρ)
      = A ^ (1 : ℝ) * A ^ ((1 - ρ) / ρ) := by rw [rpow_one]
    _ = A ^ (1 + (1 - ρ) / ρ) := (rpow_add hA_pos 1 ((1 - ρ) / ρ)).symm
    _ = A ^ (1 / ρ) := by congr 1; field_simp; ring

Dependency Graph

Location

thesis/CESProofs/Applications/Economics.lean:692

Module Section

Economics extensions for CES formalization:

In the same file