Merger Cost Duopoly Value

theorem proved Microeconomics

Documentation

Lean 4 Proof

theorem mergerCost_duopoly_value {ρ : ℝ} :
    mergerCurvatureCost 2 ρ = (1 - ρ) / 2 := by
  simp only [mergerCurvatureCost]; norm_num

Dependency Graph

Location

thesis/CESProofs/EntryExit/MarketStructure.lean:95

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 mergerCurvatureCost_eq_diff mergerCurvatureCost_pos mergerCost_duopoly_maximal mergerCurvatureCost_anti