Documentation

Lean 4 Proof

theorem curvature_decreases_on_exit {ρ H H' : ℝ}
    (hρ : ρ < 1) (hH : H < H') :
    (1 - ρ) * (1 - H') < (1 - ρ) * (1 - H) := by
  apply mul_lt_mul_of_pos_left _ (by linarith)
  linarith

Dependency Graph

Location

thesis/CESProofs/Applications/HeterogeneousFirms.lean:119

Module Section

Heterogeneous Firms and the Melitz Connection

In the same file