Documentation

Lean 4 Proof

theorem mergerCurvatureCost_pos {J ρ : ℝ} (hJ : 1 < J) (hρ : ρ < 1) :
    0 < mergerCurvatureCost J ρ := by
  simp only [mergerCurvatureCost]
  apply div_pos (by linarith)
  exact mul_pos (by linarith) (by linarith)

Dependency Graph

Location

thesis/CESProofs/EntryExit/MarketStructure.lean:77

Module Section

Paper 1, §22.5: Market Structure as CES Curvature

In the same file