Merger Term Positive

theorem proved Hierarchy

Documentation

Lean 4 Proof

theorem merger_term_positive {γ_M a_bar : ℝ}
    (hγM : 0 < γ_M) (hab : 0 < a_bar) :
    0 < γ_M * (2 * a_bar ^ 2) := by
  positivity

Dependency Graph

Location

thesis/CESProofs/Hierarchy/HerfindahlDynamics.lean:175

Module Section

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

In the same file

herfindahlIndex equalWeights herfindahl_equal_weights equalWeightH herfindahl_entry_decrease herfindahl_entry_decrease_index herfindahl_entry_change herfindahl_merger_formula herfindahl_merger_increase herfindahl_merger_max_at_equal_split herfindahl_exit_increases curvature_decreasing_in_H merger_reduces_curvature antitrust_preserves_curvature entry_term_negative merger_dominance_condition