Documentation

Lean 4 Proof

theorem sigma_gt_one {ρ : ℝ} (hρ : 0 < ρ) (hρ1 : ρ < 1) :
    1 < elasticityOfSubstitution ρ := by
  simp only [elasticityOfSubstitution]
  rw [one_lt_div (by linarith : (0 : ℝ) < 1 - ρ)]
  linarith

Dependency Graph

Used by

Location

thesis/CESProofs/Applications/Economics.lean:61

Module Section

Economics extensions for CES formalization:

In the same file