Documentation

Lean 4 Proof

theorem curvatureK_mul_sigma {J : ℕ} {ρ : ℝ} (hρ1 : ρ ≠ 1) (hJ : 0 < J) :
    curvatureK J ρ * elasticityOfSubstitution ρ = (↑J - 1) / ↑J := by
  simp only [curvatureK, elasticityOfSubstitution]
  have h : (1 : ℝ) - ρ ≠ 0 := sub_ne_zero.mpr (Ne.symm hρ1)
  have hJne : (↑J : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (Nat.pos_iff_ne_zero.mp hJ)
  field_simp [h, hJne]

Dependency Graph

Location

thesis/CESProofs/Applications/Economics.lean:356

Module Section

Economics extensions for CES formalization:

In the same file