Entry Term Negative

theorem proved Hierarchy

Documentation

Lean 4 Proof

theorem entry_term_negative {γ_E J_real : ℝ}
    (hγE : 0 < γ_E) (hJ : 0 < J_real) :
    -γ_E * (2 / J_real) < 0 := by
  apply mul_neg_of_neg_of_pos
  · linarith
  · positivity

Dependency Graph

Location

thesis/CESProofs/Hierarchy/HerfindahlDynamics.lean:166

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 merger_term_positive merger_dominance_condition