Documentation

Lean 4 Proof

theorem crs_forced {γ : ℝ} (hγ_pos : 0 < γ)
    (hγ_idem : γ ^ 2 = γ) :
    γ = 1 := by
  -- γ² = γ implies γ(γ-1) = 0
  have h : γ * (γ - 1) = 0 := by nlinarith
  rcases mul_eq_zero.mp h with h1 | h1
  · linarith -- γ = 0 contradicts γ > 0
  · linarith -- γ - 1 = 0 gives γ = 1

Dependency Graph

Location

thesis/CESProofs/Potential/IRS.lean:28

Module Section

Increasing returns to scale results (Paper 1, Section 11):

In the same file