Documentation

Lean 4 Proof

theorem lernerIndex_anti {J₁ J₂ σ : ℝ} (hJ₁ : 0 < J₁) (hσ : 0 < σ)
    (hJ : J₁ < J₂) :
    lernerIndex J₂ σ < lernerIndex J₁ σ := by
  simp only [lernerIndex]
  exact div_lt_div_of_pos_left one_pos (mul_pos hJ₁ hσ) (by nlinarith)

Dependency Graph

Location

thesis/CESProofs/EntryExit/MarketStructure.lean:53

Module Section

Paper 1, §22.5: Market Structure as CES Curvature

In the same file