Documentation

Lean 4 Proof

theorem pareto_ranking {J_high J_low ρ : ℝ}
    (hJl : 1 < J_low) (hJh : J_low < J_high) (hρ : ρ < 1) :
    -- The coordination gap in curvature is positive
    0 < coordinationGap J_high J_low ρ :=
  coordinationGap_pos hJl hJh hρ

Dependency Graph

Location

thesis/CESProofs/EntryExit/Welfare.lean:29

Module Section

Paper 1c, Section 4: Welfare and Coordination Failure

In the same file