Documentation

Lean 4 Proof

theorem strategic_complementarity {J ρ : ℝ}
    (hJ : 0 < J) (hρ : ρ < 1) :
    0 < marginalK J ρ :=
  pigouvian_subsidy_pos hJ hρ

Dependency Graph

Location

thesis/CESProofs/EntryExit/Equilibria.lean:29

Module Section

Paper 1c, Section 3: The Participation Game

In the same file