Documentation

Lean 4 Proof

theorem trade_elasticity_eq_variety_exponent {ρ : ℝ} (hρ : ρ ≠ 0) (hρ1 : ρ ≠ 1) :
    1 / (elasticityOfSubstitution ρ - 1) = 1 / ρ - 1 := by
  simp only [elasticityOfSubstitution]
  have h : (1 : ℝ) - ρ ≠ 0 := by intro h; apply hρ1; linarith
  field_simp
  have : 1 - (1 - ρ) = ρ := by ring
  rw [this]
  exact div_self hρ

Dependency Graph

Location

thesis/CESProofs/Applications/Economics.lean:332

Module Section

Economics extensions for CES formalization:

In the same file