Documentation

Lean 4 Proof

theorem strategic_complementarity_full {J ρ c : ℝ}
    (hJ : 1 < J) (hρ0 : 0 < ρ) (hρ1 : ρ < 1) (hc : 0 < c) :
    0 < valueFunctionDeriv J ρ c :=
  valueFunctionDeriv_pos hJ hρ0 hρ1 hc

Dependency Graph

Location

thesis/CESProofs/EntryExit/Equilibria.lean:37

Module Section

Paper 1c, Section 3: The Participation Game

In the same file