Documentation

Lean 4 Proof

theorem mergerCost_duopoly_maximal {J ρ : ℝ} (hJ : 2 < J) (hρ : ρ < 1) :
    mergerCurvatureCost J ρ < mergerCurvatureCost 2 ρ := by
  simp only [mergerCurvatureCost]
  have h1ρ : 0 < 1 - ρ := by linarith
  apply div_lt_div_of_pos_left h1ρ
  · positivity
  · have : 2 < J * (J - 1) := by nlinarith
    linarith

Dependency Graph

Location

thesis/CESProofs/EntryExit/MarketStructure.lean:85

Module Section

Paper 1, §22.5: Market Structure as CES Curvature

In the same file