Documentation

Lean 4 Proof

theorem curvature_decreasing_in_H {ρ H₁ H₂ : ℝ}
    (hρ : ρ < 1) (hH12 : H₁ < H₂) :
    (1 - ρ) * (1 - H₂) < (1 - ρ) * (1 - H₁) := by
  apply mul_lt_mul_of_pos_left _ (by linarith)
  linarith

Dependency Graph

Location

thesis/CESProofs/Hierarchy/HerfindahlDynamics.lean:135

Module Section

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

In the same file