Documentation

Lean 4 Proof

theorem marginal_curvature_bounded {J ρ : ℝ}
    (hJ : 1 ≤ J) (hρ : ρ < 1) :
    marginalK J ρ ≤ 1 - ρ := by
  simp only [marginalK]
  rw [div_le_iff₀ (sq_pos_of_pos (by linarith : (0:ℝ) < J))]
  nlinarith [sq_nonneg (J - 1)]

Dependency Graph

Location

thesis/CESProofs/EntryExit/Equilibria.lean:43

Module Section

Paper 1c, Section 3: The Participation Game

In the same file