Documentation

Lean 4 Proof

theorem herfindahl_exit_increases
    {a_exit J_old : ℝ} (ha : 0 < a_exit) (hJ : 1 < J_old) :
    -- Exit increases H by approximately a_exit² · J_old/(J_old - 1) > 0
    0 < a_exit ^ 2 * (J_old / (J_old - 1)) := by
  apply mul_pos (sq_pos_of_pos ha)
  apply div_pos (by linarith)
  linarith

Dependency Graph

Location

thesis/CESProofs/Hierarchy/HerfindahlDynamics.lean:119

Module Section

Herfindahl Dynamics: Entry, Exit, and Merger Effects on Concentration

In the same file