Lerner Index

def proved Microeconomics

Documentation

Lean 4 Proof

def lernerIndex (J : ℝ) (σ : ℝ) : ℝ := 1 / (J * σ)

Dependency Graph

Used by

lernerIndex_anti lernerIndex_monopoly

Location

thesis/CESProofs/EntryExit/MarketStructure.lean:28

Module Section

Paper 1, §22.5: Market Structure as CES Curvature

In the same file

cesMarkup cesMarkup_monopoly cesMarkup_anti lernerIndex_monopoly lernerIndex_anti mergerCurvatureCost mergerCurvatureCost_eq_diff mergerCurvatureCost_pos mergerCost_duopoly_maximal mergerCost_duopoly_value mergerCurvatureCost_anti