Documentation

Lean 4 Proof

theorem cesGradComponent_is_deriv {J : ℕ} (hJ : 0 < J) {ρ : ℝ} (hρ : ρ ≠ 0)
    {x : Fin J → ℝ} (hx : ∀ j, 0 < x j) (k : Fin J) :
    HasDerivAt (fun t => powerMean J ρ hρ (Function.update x k t))
               (cesGradComponent J ρ x k) (x k) := by
  simp only [powerMean, cesGradComponent]
  have hJpos : (0:ℝ) < ↑J := Nat.cast_pos.mpr hJ
  -- C = sum of x_j^ρ for j ≠ k
  set C := ∑ j ∈ (Finset.univ : Finset (Fin J)).erase k, (x j) ^ ρ with hC_def
  -- A = (1/J) * Σ x_j^ρ (also equals (1/J)*(x k^ρ + C))
  set A := (1/(↑J:ℝ)) * ∑ j : Fin J, (x j)^ρ with hA_def
  have hAxk : (1/(↑J:ℝ)) * ((x k)^ρ + C) = A := by
    rw [hA_def, hC_def]; congr 1
    have h := Finset.sum_erase_add Finset.univ (fun j => (x j)^ρ) (Finset.mem_univ k)
    linarith
  have hApos : 0 < A := mul_pos (div_pos one_pos hJpos)
    (Finset.sum_pos (fun j _ => rpow_pos_of_pos (hx j) ρ) ⟨⟨0, hJ⟩, Finset.mem_univ _⟩)
  -- Rewrite the function: updating x k to t gives inner sum = t^ρ + C
  have hfun_eq : (fun t : ℝ =>
      ((1/(↑J:ℝ)) * ∑ j : Fin J, (Function.update x k t j) ^ ρ) ^ (1/ρ)) =
      (fun t => ((1/(↑J:ℝ)) * (t ^ ρ + C)) ^ (1/ρ)) := funext (fun t => by
    congr 2
    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]
  -- Derivative of (1/J)*(t^ρ + C) at x k is (1/J)*(ρ*(x k)^(ρ-1))
  have hAd : HasDerivAt (fun t : ℝ => (1/(↑J:ℝ)) * (t^ρ + C))
      ((1/(↑J:ℝ)) * (ρ * (x k)^(ρ-1))) (x k) := by
    have h := ((hasDerivAt_id (x k)).rpow_const (p := ρ) (Or.inl (hx k).ne'))
    simp only [id, one_mul] at h
    exact (h.add_const C).const_mul (1/(↑J:ℝ))
  -- Chain rule: d/dt [f(t)^(1/ρ)] = f'(t)*(1/ρ)*f(t)^(1/ρ-1)
  have h_rpow := hAd.rpow_const (p := 1/ρ) (Or.inl (hAxk ▸ hApos).ne')
  -- Rewrite (1/J)*((x k)^ρ + C) to A in the derivative
  have hOuter := hAxk ▸ h_rpow
  -- The derivative equals cesGradComponent: (1/J)·ρ·(1/ρ) = 1/J
  have hkey : (1/(↑J:ℝ)) * (ρ * (x k)^(ρ-1)) * (1/ρ) * A ^ ((1:ℝ)/ρ - 1) =
      1/↑J * (x k)^(ρ-1) * A ^ ((1-ρ)/ρ) := by
    have h1 : (1:ℝ)/ρ - 1 = (1-ρ)/ρ := by field_simp [hρ]
    have h2 : (1/(↑J:ℝ)) * (ρ * (x k)^(ρ-1)) * (1/ρ) = 1/↑J * (x k)^(ρ-1) := by
      field_simp [hρ]
    rw [h1, h2]
  exact hkey ▸ hOuter

Dependency Graph

Location

thesis/CESProofs/Applications/Economics.lean:731

Module Section

Economics extensions for CES formalization:

In the same file