Lerner Index Monopoly

theorem proved Microeconomics

Documentation

Lean 4 Proof

theorem lernerIndex_monopoly {σ : ℝ} :
    lernerIndex 1 σ = 1 / σ := by
  simp only [lernerIndex, one_mul]

Dependency Graph

Location

thesis/CESProofs/EntryExit/MarketStructure.lean:48

Module Section

Paper 1, §22.5: Market Structure as CES Curvature

In the same file

cesMarkup lernerIndex cesMarkup_monopoly cesMarkup_anti lernerIndex_anti mergerCurvatureCost mergerCurvatureCost_eq_diff mergerCurvatureCost_pos mergerCost_duopoly_maximal mergerCost_duopoly_value mergerCurvatureCost_anti