Per Capita Surplus At Two

theorem proved Microeconomics

Documentation

Lean 4 Proof

theorem perCapitaSurplus_at_two (ρ : ℝ) :
    perCapitaSurplus 2 ρ = (1 - ρ) / 4 := by
  simp only [perCapitaSurplus]
  norm_num

Dependency Graph

Used by

multiple_equilibria_sign_below_peak multiple_equilibria_lower_root perCapitaSurplus_le_peak multiple_equilibria_upper_root

Location

thesis/CESProofs/EntryExit/Calculus.lean:178

Module Section

Paper 1c: Formal Calculus on K(J) and V(J)