Documentation

Lean 4 Proof

theorem sigma_pos {ρ : ℝ} (hρ : ρ < 1) :
    0 < elasticityOfSubstitution ρ := by
  simp only [elasticityOfSubstitution]
  exact div_pos one_pos (by linarith)

Dependency Graph

Location

thesis/CESProofs/Applications/Economics.lean:55

Module Section

Economics extensions for CES formalization:

In the same file