Documentation

Lean 4 Proof

theorem merger_dominance_condition
    {γ_E γ_M J_real a_bar : ℝ}
    (hγE : 0 < γ_E) (hγM : 0 < γ_M)
    (hJ : 0 < J_real) (hab : 0 < a_bar)
    (h_dom : γ_E < γ_M * a_bar ^ 2 * J_real) :
    γ_E * (2 / J_real) < γ_M * (2 * a_bar ^ 2) := by
  have lhs_bound : γ_E / J_real < γ_M * a_bar ^ 2 := by
    rw [div_lt_iff₀ hJ]
    linarith
  have : γ_E * (2 / J_real) = (γ_E / J_real) * 2 := by ring
  rw [this]
  nlinarith

Dependency Graph

Location

thesis/CESProofs/Hierarchy/HerfindahlDynamics.lean:183

Module Section

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

In the same file