Documentation

Lean 4 Proof

theorem welfare_gap_proportional_to_K {J_high J_low ρ : ℝ}
    (hJl : 1 < J_low) (hJh : J_low < J_high) (hρ : ρ < 1)
    (benefit : ℝ) (hb : 0 < benefit) :
    0 < coordinationGap J_high J_low ρ * benefit := by
  exact mul_pos (coordinationGap_pos hJl hJh hρ) hb

Dependency Graph

Location

thesis/CESProofs/EntryExit/Welfare.lean:38

Module Section

Paper 1c, Section 4: Welfare and Coordination Failure

In the same file