Documentation

Lean 4 Proof

theorem mergerCurvatureCost_anti {J₁ J₂ ρ : ℝ}
    (hJ₁ : 1 < J₁) (hρ : ρ < 1) (hJ : J₁ < J₂) :
    mergerCurvatureCost J₂ ρ < mergerCurvatureCost J₁ ρ := by
  simp only [mergerCurvatureCost]
  have h1ρ : 0 < 1 - ρ := by linarith
  apply div_lt_div_of_pos_left h1ρ
  · exact mul_pos (by linarith) (by linarith)
  · nlinarith

Dependency Graph

Location

thesis/CESProofs/EntryExit/MarketStructure.lean:101

Module Section

Paper 1, §22.5: Market Structure as CES Curvature

In the same file