Per Capita Surplus At One

theorem proved Microeconomics

Documentation

Lean 4 Proof

theorem perCapitaSurplus_at_one (ρ : ℝ) :
    perCapitaSurplus 1 ρ = 0 := by
  simp [perCapitaSurplus]

Dependency Graph

Used by

multiple_equilibria_sign_below_peak multiple_equilibria_lower_root

Location

thesis/CESProofs/EntryExit/Calculus.lean:173

Module Section

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