Documentation

Lean 4 Proof

theorem ces_limit_cobbDouglas {J : ℕ} (hJ : 0 < J) {x : Fin J → ℝ} (hx : ∀ j, 0 < x j) :
    Filter.Tendsto
      (fun ρ : ℝ => ((1 / (↑J : ℝ)) * ∑ j : Fin J, (x j) ^ ρ) ^ (1 / ρ))
      (nhdsWithin 0 (Set.Ioi 0))
      (nhds (geometricMean J x)) := by
  set A : ℝ → ℝ := fun ρ => (1 / (↑J : ℝ)) * ∑ j : Fin J, (x j) ^ ρ with hA_def
  set D := (1 / (↑J : ℝ)) * ∑ j : Fin J, Real.log (x j)
  have hJpos : (0 : ℝ) < ↑J := Nat.cast_pos.mpr hJ
  have hAd := ces_inner_hasDerivAt hJ hx
  have hA0 : A 0 = 1 := by simp [A, rpow_zero, hJ.ne']
  have hApos : ∀ ρ, 0 < A ρ := fun ρ =>
    mul_pos (div_pos one_pos hJpos)
      (Finset.sum_pos (fun j _ => rpow_pos_of_pos (hx j) ρ) ⟨⟨0, hJ⟩, Finset.mem_univ _⟩)
  -- log A(ρ) has derivative D at 0 (chain rule: (log A)'(0) = A'(0)/A(0) = D/1 = D)
  have hlogAd : HasDerivAt (fun ρ => Real.log (A ρ)) D 0 := by
    have h := (hasDerivAt_log (hApos 0).ne').comp 0 hAd
    simp only [hA0, inv_one, one_mul] at h
    exact h
  have hlogA0 : Real.log (A 0) = 0 := by rw [hA0]; exact log_one
  -- log A(ρ)/ρ → D as ρ → 0+ (this is the "0/0" limit resolved by the derivative)
  have hslope : Filter.Tendsto (fun ρ => Real.log (A ρ) / ρ)
      (nhdsWithin 0 (Set.Ioi 0)) (nhds D) := by
    have hts := hasDerivAt_iff_tendsto_slope.mp hlogAd
    have hmono : nhdsWithin (0 : ℝ) (Set.Ioi 0) ≤ nhdsWithin 0 {0}ᶜ :=
      nhdsWithin_mono 0 (fun _ hρ => hρ.ne')
    exact (hts.mono_left hmono).congr'
      (eventually_nhdsWithin_of_forall (fun ρ _ => by
        simp only [slope_def_field, hlogA0, sub_zero]))
  -- exp(D) = geometricMean J x
  have hexpD : Real.exp D = geometricMean J x := by
    simp only [geometricMean]
    rw [show D = (1 / (↑J : ℝ)) * ∑ j : Fin J, Real.log (x j) from rfl,
        ← Real.log_prod (fun j _ => (hx j).ne'),
        Real.rpow_def_of_pos (Finset.prod_pos (fun j _ => hx j))]
    congr 1; ring
  -- Conclude: A(ρ)^{1/ρ} = exp(log A(ρ)/ρ) → exp(D) = geometricMean
  rw [← hexpD]
  exact ((Real.continuous_exp.continuousAt.tendsto).comp hslope).congr'
    (eventually_nhdsWithin_of_forall (fun ρ _ => by
      simp only [Function.comp, A, rpow_def_of_pos (hApos _)]
      congr 1; ring))

Dependency Graph

Location

thesis/CESProofs/Applications/Economics.lean:821

Module Section

Economics extensions for CES formalization:

In the same file