Documentation

Lean 4 Proof

theorem dualExponent_eq_sigma {ρ : ℝ} (hρ : ρ ≠ 1) :
    dualExponent ρ = 1 - elasticityOfSubstitution ρ := by
  simp only [dualExponent, elasticityOfSubstitution]
  have h : (1 : ℝ) - ρ ≠ 0 := by intro h; apply hρ; linarith
  have h' : ρ - (1 : ℝ) ≠ 0 := by intro h'; apply hρ; linarith
  field_simp
  ring

Dependency Graph

Used by

Location

thesis/CESProofs/Applications/Economics.lean:89

Module Section

Economics extensions for CES formalization:

In the same file