Merger Curvature Cost

def proved Microeconomics

Documentation

Lean 4 Proof

def mergerCurvatureCost (J : ℝ) (ρ : ℝ) : ℝ := (1 - ρ) / (J * (J - 1))

Dependency Graph

Used by

mergerCurvatureCost_anti mergerCost_duopoly_maximal mergerCost_duopoly_value mergerCurvatureCost_eq_diff mergerCurvatureCost_pos

Location

thesis/CESProofs/EntryExit/MarketStructure.lean:65

Module Section

Paper 1, §22.5: Market Structure as CES Curvature

In the same file

cesMarkup lernerIndex cesMarkup_monopoly cesMarkup_anti lernerIndex_monopoly lernerIndex_anti mergerCurvatureCost_eq_diff mergerCurvatureCost_pos mergerCost_duopoly_maximal mergerCost_duopoly_value mergerCurvatureCost_anti