Documentation

Lean 4 Proof

theorem underentry_proved {J ρ c κ : ℝ}
    (hJ : 1 < J) (hρ0 : 0 < ρ) (hρ1 : ρ < 1) (hc : 0 < c)
    (hFOC : valueFunction J ρ c = κ) :
    κ < valueFunction J ρ c + J * valueFunctionDeriv J ρ c :=
  underentry_at_private_optimum hJ hρ0 hρ1 hc hFOC

Dependency Graph

Location

thesis/CESProofs/EntryExit/Welfare.lean:55

Module Section

Paper 1c, Section 4: Welfare and Coordination Failure

In the same file