Documentation

Lean 4 Proof

theorem cesMarkup_anti {J₁ J₂ σ : ℝ} (_hJ₁ : 0 < J₁) (hσ : 1 < σ)
    (hJ : J₁ < J₂) (hJσ₁ : 1 < J₁ * σ) :
    cesMarkup J₂ σ < cesMarkup J₁ σ := by
  simp only [cesMarkup]
  have hσ₀ : 0 < σ := by linarith
  have hJσ₂ : 1 < J₂ * σ := lt_trans hJσ₁ (by nlinarith)
  have h₁ : 0 < J₁ * σ - 1 := by linarith
  have h₂ : 0 < J₂ * σ - 1 := by linarith
  rw [div_lt_div_iff₀ h₂ h₁]
  nlinarith

Dependency Graph

Location

thesis/CESProofs/EntryExit/MarketStructure.lean:36

Module Section

Paper 1, §22.5: Market Structure as CES Curvature

In the same file