Documentation

Lean 4 Proof

theorem mergerCurvatureCost_eq_diff {J ρ : ℝ} (hJ : 1 < J) (hJne : J ≠ 0) :
    mergerCurvatureCost J ρ = curvatureKReal J ρ - curvatureKReal (J - 1) ρ := by
  simp only [mergerCurvatureCost, curvatureKReal]
  have hJm1 : J - 1 ≠ 0 := by linarith
  have hJJm1 : J * (J - 1) ≠ 0 := mul_ne_zero hJne hJm1
  field_simp [hJne, hJm1, hJJm1]
  ring

Dependency Graph

Location

thesis/CESProofs/EntryExit/MarketStructure.lean:68

Module Section

Paper 1, §22.5: Market Structure as CES Curvature

In the same file