Documentation

Lean 4 Proof

theorem curvatureK_eq_sigma (ρ : ℝ) :
    curvatureK J ρ = (1 / elasticityOfSubstitution ρ) * (↑J - 1) / ↑J := by
  simp only [curvatureK, elasticityOfSubstitution]
  rw [one_div, one_div, inv_inv]

Dependency Graph

Location

thesis/CESProofs/Applications/Economics.lean:83

Module Section

Economics extensions for CES formalization:

In the same file