Documentation

Lean 4 Proof

theorem cesMarkup_monopoly {σ : ℝ} (_hσ : 1 < σ) :
    cesMarkup 1 σ = σ / (σ - 1) := by
  simp only [cesMarkup, one_mul]

Dependency Graph

Location

thesis/CESProofs/EntryExit/MarketStructure.lean:31

Module Section

Paper 1, §22.5: Market Structure as CES Curvature

In the same file