CES Markup

def proved Microeconomics

Documentation

Lean 4 Proof

def cesMarkup (J : ℝ) (σ : ℝ) : ℝ := J * σ / (J * σ - 1)

Dependency Graph

Used by

cesMarkup_anti cesMarkup_monopoly

Location

thesis/CESProofs/EntryExit/MarketStructure.lean:24

Module Section

Paper 1, §22.5: Market Structure as CES Curvature

In the same file

lernerIndex cesMarkup_monopoly cesMarkup_anti lernerIndex_monopoly lernerIndex_anti mergerCurvatureCost mergerCurvatureCost_eq_diff mergerCurvatureCost_pos mergerCost_duopoly_maximal mergerCost_duopoly_value mergerCurvatureCost_anti