Documentation

Lean 4 Proof

theorem cournot_overinvestment {a b : ℝ} {N : ℕ}
    (ha : 0 < a) (hb : 0 < b) (hN : 2 ≤ N) :
    a / (2 * b) < ↑N * a / ((↑N + 1) * b) := by
  have hN_ge2 : (2 : ℝ) ≤ ↑N := by exact_mod_cast hN
  have h2b : (0 : ℝ) < 2 * b := by positivity
  have hNb : (0 : ℝ) < (↑N + 1) * b := by positivity
  rw [div_lt_div_iff₀ h2b hNb]
  -- Goal: a * ((↑N + 1) * b) < ↑N * a * (2 * b)
  -- Simplifies to (N+1) < 2N, i.e., 1 < N
  have hab : 0 < a * b := mul_pos ha hb
  nlinarith [mul_pos ha hb]

Dependency Graph

Location

thesis/CESProofs/Hierarchy/EndogenousCrossing.lean:211

Module Section

Proposition: Endogenous Crossing

In the same file