Documentation

Lean 4 Proof

theorem gainsFromVariety_eq_trade_gains {J : ℕ} {ρ : ℝ}
    (hρ : ρ ≠ 0) (hρ1 : ρ ≠ 1) :
    gainsFromVariety J ρ = (↑J : ℝ) ^ (1 / (elasticityOfSubstitution ρ - 1)) := by
  simp only [gainsFromVariety, elasticityOfSubstitution]
  congr 1
  have h : (1 : ℝ) - ρ ≠ 0 := sub_ne_zero.mpr (Ne.symm hρ1)
  field_simp [hρ, h]
  ring

Dependency Graph

Location

thesis/CESProofs/Applications/Economics.lean:288

Module Section

Economics extensions for CES formalization:

In the same file