Documentation

Lean 4 Proof

theorem ces_inner_hasDerivAt {J : ℕ} (_hJ : 0 < J) {x : Fin J → ℝ} (hx : ∀ j, 0 < x j) :
    HasDerivAt (fun (ρ : ℝ) => (1 / (J : ℝ)) * ∑ j : Fin J, (x j) ^ ρ)
      ((1 / (J : ℝ)) * ∑ j : Fin J, Real.log (x j)) (0 : ℝ) := by
  -- Each x_j^rho has derivative log(x_j) at rho = 0
  have hderiv' : ∀ j : Fin J,
      HasDerivAt (fun (ρ : ℝ) => (x j) ^ ρ) (Real.log (x j)) (0 : ℝ) := by
    intro j
    have h := HasDerivAt.const_rpow (hx j) (hasDerivAt_id (0 : ℝ))
    convert h using 1; simp [Real.rpow_zero]
  -- Sum of derivatives (fun_sum matches lambda form)
  have hsum : HasDerivAt (fun (ρ : ℝ) => ∑ j : Fin J, (x j) ^ ρ)
      (∑ j : Fin J, Real.log (x j)) (0 : ℝ) :=
    HasDerivAt.fun_sum (fun j _ => hderiv' j)
  -- Multiply by constant 1/J
  exact hsum.const_mul (1 / (J : ℝ))

Dependency Graph

Used by

Location

thesis/CESProofs/Applications/Economics.lean:798

Module Section

Economics extensions for CES formalization:

In the same file