Documentation

Lean 4 Proof

theorem sigma_rho_inverse {ρ : ℝ} (hρ : ρ ≠ 1) :
    ρ = 1 - 1 / elasticityOfSubstitution ρ := by
  simp only [elasticityOfSubstitution]
  have h : (1 : ℝ) - ρ ≠ 0 := by intro h; apply hρ; linarith
  field_simp
  linarith

Dependency Graph

Location

thesis/CESProofs/Applications/Economics.lean:74

Module Section

Economics extensions for CES formalization:

In the same file